|
Local Model Checking and Traces
Allan Cheng June 1994 |
Abstract:
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.
Notice! Please refer to the revised version BRICS-RS-95-39.
|