Temporal Epistemic Logic is used to reason about the evolution of knowledge over time. A notable example is the temporal epistemic logic KL1, which is used to model what a reasoner can infer about the state of a dynamic system by using available observations. Applications of KL1 span from security (verification of cryptography protocols and information flow) to diagnostic systems (fault detection and diagnosability). In this paper, we tackle the verification of KL1 properties under observational semantics, by proposing an effective approach that is able to deal with both finite and infinite state systems. The denotation of the epistemic atoms is computed in a lazy way, driven by the counter-examples obtained from model checking an abstraction of the property. We analyze the approach on a comprehensive set of finite- and infinite-state benchmarks from the literature, evaluate the effectiveness of various optimizations, and demonstrate that our approach outperforms existing approaches.
A Lazy Approach to Temporal Epistemic Logic Model Checking
Cimatti, Alessandro;Gario, Marco Elio Gustavo;Tonetta, Stefano
2016-01-01
Abstract
Temporal Epistemic Logic is used to reason about the evolution of knowledge over time. A notable example is the temporal epistemic logic KL1, which is used to model what a reasoner can infer about the state of a dynamic system by using available observations. Applications of KL1 span from security (verification of cryptography protocols and information flow) to diagnostic systems (fault detection and diagnosability). In this paper, we tackle the verification of KL1 properties under observational semantics, by proposing an effective approach that is able to deal with both finite and infinite state systems. The denotation of the epistemic atoms is computed in a lazy way, driven by the counter-examples obtained from model checking an abstraction of the property. We analyze the approach on a comprehensive set of finite- and infinite-state benchmarks from the literature, evaluate the effectiveness of various optimizations, and demonstrate that our approach outperforms existing approaches.File | Dimensione | Formato | |
---|---|---|---|
camera_ready.pdf
solo utenti autorizzati
Tipologia:
Documento in Pre-print
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
267.53 kB
Formato
Adobe PDF
|
267.53 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.