Abstract :
[en] This paper presents a model-checking method for linear-time temporal logic that avoids the state explosion due to the modelling 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
Scopus citations®
without self-citations
94
