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.
2016
978-1-4503-4239-1
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/306073
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact