A partial approach to model checking. (English) Zbl 0806.68079
Summary: This paper presents a model-checking method for linear-time temporal logic that can avoid most of the state explosion due to the modeling of concurrency by interleaving. The method relies on the concept of Mazurkiewicz’s trace as a semantic basis and uses automata-theoretic techniques, including automata that operate on words of ordinality higher than \(\omega\).
MSC:
68Q60 | Specification and verification (program logics, model checking, etc.) |
68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |
68Q45 | Formal languages and automata |
03B70 | Logic in computer science |