Další formáty:
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, s.~222-229.
|
