Other formats:
BibTeX
LaTeX
RIS
@inproceedings{704336, author = {Šimša, Jiří}, address = {Mikulov, Czech Republic}, booktitle = {2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006)}, keywords = {model checking; linear temporal logic; tableau construction}, language = {eng}, location = {Mikulov, Czech Republic}, pages = {222-229}, publisher = {FI MU Report Series}, title = {On Alternative Construction of LTL Tableau}, year = {2006} }
TY - JOUR ID - 704336 AU - Šimša, Jiří PY - 2006 TI - On Alternative Construction of LTL Tableau PB - FI MU Report Series CY - Mikulov, Czech Republic KW - model checking KW - linear temporal logic KW - tableau construction N2 - 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. ER -
ŠIMŠA, Jiří. On Alternative Construction of LTL Tableau. In \textit{2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006)}. Mikulov, Czech Republic: FI MU Report Series, 2006, p.~222-229.
|