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 metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01527383
Contributor : Hal Ifip <>
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

File

978-3-642-28038-2_13_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

99

Files downloads

102