"Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines

Petra Kaufmann; Andreas Pfandler; Martin Kronegger; Martina Seidl; Magdalena Widl

"Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines

Petra Kaufmann, Andreas Pfandler, Martin Kronegger, Martina Seidl, Magdalena Widl

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

We present a novel propositional encoding for the reachability problem of communicating state machines. The problem deals with the question whether there is a path to some combination of states in a state machine view starting from a given configuration. Reachability analysis finds its application in many verification scenarios. By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the reachability problem in propositional logic. We present the formal framework for our encoding and a prototype implementation. A first case study underpins its effectiveness.

Original language	English
Title of host publication	Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation
Pages	31-40
Number of pages	10
Volume	1069
Publication status	Published - Jan 2013

Publication series

Name	CEUR Workshop Proceedings
ISSN (Print)	1613-0073

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{8a5a120943e64001b60b4142d5233a8e,

title = "{"}Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines",

abstract = "We present a novel propositional encoding for the reachability problem of communicating state machines. The problem deals with the question whether there is a path to some combination of states in a state machine view starting from a given configuration. Reachability analysis finds its application in many verification scenarios. By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the reachability problem in propositional logic. We present the formal framework for our encoding and a prototype implementation. A first case study underpins its effectiveness.",

author = "Petra Kaufmann and Andreas Pfandler and Martin Kronegger and Martina Seidl and Magdalena Widl",

year = "2013",

month = jan,

language = "English",

volume = "1069",

series = "CEUR Workshop Proceedings",

pages = "31--40",

booktitle = "Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation",

}

"Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines. / Kaufmann, Petra; Pfandler, Andreas; Kronegger, Martin et al.
Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation. Vol. 1069 2013. p. 31-40 (CEUR Workshop Proceedings).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - "Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines

AU - Kaufmann, Petra

AU - Pfandler, Andreas

AU - Kronegger, Martin

AU - Seidl, Martina

AU - Widl, Magdalena

PY - 2013/1

Y1 - 2013/1

N2 - We present a novel propositional encoding for the reachability problem of communicating state machines. The problem deals with the question whether there is a path to some combination of states in a state machine view starting from a given configuration. Reachability analysis finds its application in many verification scenarios. By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the reachability problem in propositional logic. We present the formal framework for our encoding and a prototype implementation. A first case study underpins its effectiveness.

AB - We present a novel propositional encoding for the reachability problem of communicating state machines. The problem deals with the question whether there is a path to some combination of states in a state machine view starting from a given configuration. Reachability analysis finds its application in many verification scenarios. By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the reachability problem in propositional logic. We present the formal framework for our encoding and a prototype implementation. A first case study underpins its effectiveness.

M3 - Conference proceedings

VL - 1069

T3 - CEUR Workshop Proceedings

SP - 31

EP - 40

BT - Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation

ER -