On the Expressive Power of the Normal Form for Branching-Time Temporal Logics

Alexander Bolotov
(University of Westminster)

With the emerging applications that involve complex distributed systems branching-time specifications are specifically important as they reflect dynamic and non-deterministic nature of such applications. We describe the expressive power of a simple yet powerful branching-time specification framework – branching-time normal form (BNF), which has been developed as part of clausal resolution for branching-time temporal logics. We show the encoding of Buchi Tree Automata in the language of the normal form, thus representing, syntactically, tree automata in a high-level way. Thus we can treat BNF as a normal form for the latter. These results enable us (1) to translate given problem specifications into the normal form and apply as a verification method a deductive reasoning technique – the clausal temporal resolution; (2) to apply one of the core components of the resolution method - the loop searching to extract, syntactically, hidden invariants in a wide range of complex temporal specifications.

In Andrzej Indrzejczak and Michał Zawidzki: Proceedings of the 10th International Conference on Non-Classical Logics. Theory and Applications (NCL 2022), Łódź, Poland, 14-18 March 2022, Electronic Proceedings in Theoretical Computer Science 358, pp. 254–269.
Published: 14th April 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.358.19 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org