Open AccessLocal Model Checking and Traces
Author(s) -
Allan Cheng
Publication year - 1994
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v1i17.21650
Subject(s) - soundness , decidability , model checking , completeness (order theory) , interpretation (philosophy) , temporal logic , boolean satisfiability problem , asynchronous communication , satisfiability , theoretical computer science , mathematics , computer science , ctl* , set (abstract data type) , abstraction model checking , discrete mathematics , algorithm , programming language , mathematical analysis , computer network , biochemistry , chemistry , cytotoxic t cell , in vitro
We present a CTL -like logic which is interpreted over labeled asynchronous transition systems. The interpretation reflects the desire to reason about these only with respect their progress fair behaviours. For finite systems we provide a set of tableau rules and prove soundness and completeness with respect to the given interpretation of our logic. We also provide a model checking algorithm which solves the model checking problem in deterministic polynomial time in the size of the formula and the labelled asynchronous transition system. We then consider different extensions of the logic with modalities expressing concurrent behaviour and investigate how this affects the decidability of the satisfiability problem.