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

&
Synthese 142 (2):203-227 (2004)
  Copy   BIBTEX

Abstract

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.

Categories

Keywords

Reprint years

2005

DOI

10.1007/s11229-004-2446-8

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications.Wiebe van der Hoek & Michael Wooldridge - 2003 - Studia Logica 75 (1):125-157.
Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and Its Applications.Wiebe van Der Hoek & Michael Wooldridge - 2003 - Studia Logica 75 (1):125-157.
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.
Comparing semantics of logics for multi-agent systems.Valentin Goranko & Wojciech Jamroga - 2004 - Synthese 139 (2):241 - 280.
Checking EMTLK Properties of Timed Interpreted Systems Via Bounded Model Checking.Bożena Woźna-Szcześniak & Andrzej Zbrzezny - 2016 - Studia Logica 104 (4):641-678.
Logics of temporal-epistemic actions.Bryan Renne, Joshua Sack & Audrey Yap - 2016 - Synthese 193 (3):813-849.
An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking.Dimitar P. Guelev, Catalin Dima & Constantin Enea - 2011 - Journal of Applied Non-Classical Logics 21 (1):93-131.
Social laws in alternating time: Effectiveness, feasibility, and synthesis.Wiebe van der Hoek, Mark Roberts & Michael Wooldridge - 2007 - Synthese 156 (1):1-19.
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.
Constructive knowledge: what agents can achieve under imperfect information.Wojciech Jamroga & Thomas Ågotnes - 2007 - Journal of Applied Non-Classical Logics 17 (4):423-475.
Verifying Temporal Heap Properties Specified via Evolution Logic.E. Yahav, T. Reps, M. Sagiv & R. Wilhelm - 2006 - Logic Journal of the IGPL 14 (5):755-783.
Model checking for hybrid logic.Martin Lange - 2009 - Journal of Logic, Language and Information 18 (4):465-491.
Model checking techniqes for the analysis of reactive systems.Stephan Merz - 2002 - Synthese 133 (1-2):173 - 201.
An infinitary variant of Metric Temporal Logic over dense time domains.S. Baratella - 2004 - Mathematical Logic Quarterly 50 (3):249.

Analytics

Added to PP
2009-01-28

Downloads
43 (#361,277)

6 months
5 (#629,136)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Add more citations

References found in this work

Add more references