On Alternative Construction of LTL Tableau
| Authors | |
|---|---|
| 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 | |
| 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: |