A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic

Synthese 142 (2):203-227 (2004)
This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Epistemic Logic (ATEL) is used for expressing properties of multi-agent systems represented by alternating epistemic temporal systems as well as concurrent epistemic game structures. Unbounded model checking (a SAT based technique) is applied for the first time to verification of ATEL. An example is given to show an application of the technique.
Keywords Philosophy   Philosophy   Epistemology   Logic   Metaphysics   Philosophy of Language
Categories (categorize this paper)
Reprint years 2005
DOI 10.1007/s11229-004-2446-8
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 37,988
Through your library

References found in this work BETA

Reasoning About Knowledge.Ronald Fagin (ed.) - 1995 - MIT Press.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Alternating Automata and Temporal Logic Normal Forms.Clare Dixon, Alexander Bolotov & Michael Fisher - 2005 - Annals of Pure and Applied Logic 135 (1-3):263-285.
A Decidable Timeout-Based Extension of Linear Temporal Logic.Janardan Misra & Suman Roy - 2014 - Journal of Applied Non-Classical Logics 24 (3):262-291.
Linear, Branching Time and Joint Closure Semantics for Temporal Logic.Joeri Engelfriet & Jan Treur - 2002 - Journal of Logic, Language and Information 11 (4):389-425.
Model Checking for Hybrid Logic.Martin Lange - 2009 - Journal of Logic, Language and Information 18 (4):465-491.


Added to PP index

Total views
32 ( #210,199 of 2,312,429 )

Recent downloads (6 months)
1 ( #469,789 of 2,312,429 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature