On Alternative Construction of LTL Tableau

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ŠIMŠA Jiří

Year of publication 2006
Type Article in Proceedings
Conference 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords model checking; linear temporal logic; tableau construction
Description Linear Temporal Logic (LTL) is a well established and extensively studied formalism in the field of formal verification. In certain applications of LTL, such as model-checking, it is convenient to identify a formula of LTL with an automata that accepts precisely the inputs that satisfy the formula. In this paper, we adopt this, automata-theoretic, approach and present a construction of such an automata. Unlike other existing constructions, our construction is based on the idea of iterative formula unfolding and normalization.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.