Skip to Main content Skip to Navigation
New interface
Conference papers

Bounded Model Checking for the Existential Part of Real-Time CTL and Knowledge

Abstract : A considerably large class of multi-agent systems operate in distributed and real-time environments, and often their correctness specifications require us to express time-critical properties that depend on performed actions of the system. In the paper, we focus on the formal verification of such systems by means of the bounded model checking (BMC) method, where specifications are expressed in the existential fragment of the Real-Time Computation Tree Logic augmented to include standard epistemic operators.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2017 - 12:48:55 PM
Last modification on : Wednesday, May 24, 2017 - 2:18:01 PM
Long-term archiving on: : Monday, August 28, 2017 - 5:12:52 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Bożena Woźna-Szcześniak. Bounded Model Checking for the Existential Part of Real-Time CTL and Knowledge. 4th Central and East European Conference on Software Engineering Techniques (CEESET), Oct 2009, Krakow, Poland. pp.164-178, ⟨10.1007/978-3-642-28038-2_13⟩. ⟨hal-01527383⟩



Record views


Files downloads