cb7bdf8c1f
This follows from a discussion with Ernesto Posse.
The semantics for the {...} operator we use in Spot comes from the
cl(...) operator defined by Dax et al. (ATVA'09). This is slightly
different from the the way the PSL spec interprets a SERE used in the
context of a temporal formula (appendix B.3.1.1.2, item 7).
cl({a;b}[*]) would match any infinite word that starts with a;b, while
in PSL {a;b}[*] would match any infinite word that alternates a and b.
Spot documents that {SERE} in a temporal formula is interpreted like
cl(SERE) however it failed to ignore the empty prefix of SERE. So
{{a;b}[*]} would match anything, because the empty word is a prefix of
any word, and is also accepted by {a;b}[*]. Some trivial identities
and basic rewritings were also wrongly considering these empty
prefixes as well.
This patch therefore fixes the translation and syntactic
simplification rules, to really ignore these empty prefixes.
In some future version it should probably be wise to rename this {...}
operator as cl(...), and use {...} for the semantics given in appendix
B.3.1.1.2 (item 7) of the PSL specs.
* src/ltlast/unop.cc: Fix trivial identities. We have
{[*0]} = 0 and !{[*0]} = 1.
* src/ltlvisit/simplify.cc: Fix basic rewriting rules.
{e[*]} = {e} and !{e[*]} = !{e}.
* doc/tl/tl.tex: Adjust documentation.
* doc/tl/tl.bib (dax.09.atva): New entry.
* src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
infinite word for {e[*]} just because the empty
prefix is matched by e[*].
* src/tgbatest/ltl2tgba.test: Add a test case.
* NEWS: Mention it.
* THANKS: Add Ernesto.
221 lines
7.2 KiB
BibTeX
221 lines
7.2 KiB
BibTeX
|
|
@InProceedings{ babiak.12.tacas,
|
|
author = {Thom{\'a}{\v{s}} Babiak and Mojm{\'i}r
|
|
K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}e}eh{\'a}k
|
|
and Jan Strej{\v c}ek},
|
|
title = {{LTL} to {B\"u}chi Automata Translation: Fast and More
|
|
Deterministic},
|
|
year = 2012,
|
|
booktitle = {Proceedings of the 18th International Conference on Tools
|
|
and Algorithms for the Construction and Analysis of Systems
|
|
(TACAS'12)},
|
|
publisher = {Springer},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = {7214},
|
|
pages = {95--109}
|
|
}
|
|
|
|
@InProceedings{ beer.01.cav,
|
|
author = {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana
|
|
Fisman and Anna Gringauze and Yoav Rodeh},
|
|
title = {The Temporal Logic {S}ugar},
|
|
booktitle = {Proceedings of the 13th international conferance on
|
|
Computer Aided Verification (CAV'01)},
|
|
series = {Lecture Notes in Computer Science},
|
|
editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain},
|
|
publisher = {Springer},
|
|
isbn = {978-3-540-42345-4},
|
|
pages = {363--367},
|
|
volume = {2102},
|
|
year = {2001},
|
|
month = jul
|
|
}
|
|
|
|
@Article{ bruggeman.96.tcs,
|
|
author = {Anne Br{\"u}ggemann-Klein},
|
|
title = {Regular Expressions into Finite Automata},
|
|
journal = {Theoretical Computer Science},
|
|
year = {1996},
|
|
volume = {120},
|
|
pages = {87--98}
|
|
}
|
|
|
|
@InProceedings{ cerna.03.mfcs,
|
|
author = {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek},
|
|
title = {Relating Hierarchy of Temporal Properties to Model
|
|
Checking},
|
|
booktitle = {Proceedings of the 28th International Symposium on
|
|
Mathematical Foundations of Computer Science (MFCS'03)},
|
|
pages = {318--327},
|
|
year = {2003},
|
|
editor = {Branislav Rovan and Peter Vojt{\'a}{\v{a}}},
|
|
volume = {2747},
|
|
series = {Lecture Notes in Computer Science},
|
|
address = {Bratislava, Slovak Republic},
|
|
month = aug,
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
@InProceedings{ chang.92.icalp,
|
|
author = {Edward Y. Chang and Zohar Manna and Amir Pnueli},
|
|
title = {Characterization of Temporal Property Classes},
|
|
booktitle = {Proceedings of the 19th International Colloquium on
|
|
Automata, Languages and Programming (ICALP'92)},
|
|
year = {1992},
|
|
pages = {474--486},
|
|
publisher = {Springer-Verlag},
|
|
address = {London, UK}
|
|
}
|
|
|
|
@Article{ cimatti.08.tcad,
|
|
author = {Alessandro Cimatti and Marco Roveri and Stefano Tonetta},
|
|
journal = {IEEE Transactions on Computer Aided Design of Integrated
|
|
Circuits and Systems},
|
|
number = 10,
|
|
pages = {1737--1750},
|
|
title = {Symbolic Compilation of PSL},
|
|
volume = 27,
|
|
year = 2008,
|
|
date = {2009-03-20},
|
|
note = {\url{https://es.fbk.eu/people/tonetta/tests/tcad07/}}
|
|
}
|
|
|
|
@InProceedings{ dax.09.atva,
|
|
author = {Christian Dax and Felix Klaedtke and Stefan Leue},
|
|
title = {Specification Languages for Stutter-Invariant Regular
|
|
Properties},
|
|
booktitle = {Proceedings of the 7th International Symposium on
|
|
Automated Technology for Verification and Analysis
|
|
(ATVA'09)},
|
|
pages = {244--254},
|
|
year = {2009},
|
|
volume = {5799},
|
|
series = {Lecture Notes in Computer Science},
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
@InProceedings{ duret.11.vecos,
|
|
author = {Alexandre Duret-Lutz},
|
|
title = {{LTL} Translation Improvements in {Spot}},
|
|
booktitle = {Proceedings of the 5th International Workshop on
|
|
Verification and Evaluation of Computer and Communication
|
|
Systems (VECoS'11)},
|
|
year = {2011},
|
|
series = {Electronic Workshops in Computing},
|
|
address = {Tunis, Tunisia},
|
|
month = sep,
|
|
publisher = {British Computer Society},
|
|
abstract = {Spot is a library of model-checking algorithms. This paper
|
|
focuses on the module translating LTL formul{\ae} into
|
|
automata. We discuss improvements that have been
|
|
implemented in the last four years, we show how Spot's
|
|
translation competes on various benchmarks, and we give
|
|
some insight into its implementation.},
|
|
url = {http://ewic.bcs.org/category/15853}
|
|
}
|
|
|
|
@Book{ eisner.06.psl,
|
|
author = {Cindy Eisner and Dana Fisman},
|
|
title = {A Practical Introduction to {PSL}},
|
|
publisher = {Springer},
|
|
year = {2006},
|
|
series = {Series on Integrated Circuits and Systems}
|
|
}
|
|
|
|
@InCollection{ eisner.08.hvc,
|
|
author = {Cindy Eisner and Dana Fisman},
|
|
title = {Structural Contradictions},
|
|
booktitle = {Proceedings of the 4th International Haifa Verification
|
|
Conference (HVC'2008)},
|
|
series = {Lecture Notes in Computer Science},
|
|
editor = {Hana Chockler and Alan Hu},
|
|
publisher = {Springer},
|
|
isbn = {978-3-642-01701-8},
|
|
pages = {164--178},
|
|
volume = {5394},
|
|
year = {2009},
|
|
month = oct
|
|
}
|
|
|
|
@InProceedings{ etessami.00.concur,
|
|
author = {Kousha Etessami and Gerard J. Holzmann},
|
|
title = {Optimizing {B\"u}chi Automata},
|
|
booktitle = {Proceedings of the 11th International Conference on
|
|
Concurrency Theory (Concur'00)},
|
|
pages = {153--167},
|
|
year = {2000},
|
|
editor = {C. Palamidessi},
|
|
volume = {1877},
|
|
series = {Lecture Notes in Computer Science},
|
|
address = {Pennsylvania, USA},
|
|
publisher = {Springer-Verlag},
|
|
note = {Beware of a typo in the version from the proceedings: $f
|
|
\U g$ is purely eventual if both operands are purely
|
|
eventual. The revision of the paper available at
|
|
\url{http://www.bell-labs.com/project/TMP/} is fixed. We
|
|
fixed the bug in Spot in 2005, thanks to LBTT. See also
|
|
\url{http://arxiv.org/abs/1011.4214v2} for a discussion
|
|
about this problem.}
|
|
}
|
|
|
|
@InProceedings{ manna.87.podc,
|
|
author = {Zohar Manna and Amir Pnueli},
|
|
title = {A hierarchy of temporal properties},
|
|
booktitle = {Proceedings of the sixth annual ACM Symposium on
|
|
Principles of distributed computing (PODC'90)},
|
|
year = {1990},
|
|
location = {Quebec City, Canada},
|
|
pages = {377--410},
|
|
publisher = {ACM},
|
|
address = {New York, NY, USA}
|
|
}
|
|
|
|
@Book{ psl.04.lrm,
|
|
title = {Property Specification Language Reference Manual v1.1},
|
|
publisher = {Accellera},
|
|
year = {2004},
|
|
month = jun,
|
|
note = {\url{http://www.eda.org/vfv/}}
|
|
}
|
|
|
|
@InProceedings{ schneider.01.lpar,
|
|
author = {Klaus Schneider},
|
|
title = {Improving Automata Generation for Linear Temporal Logic by
|
|
Considering the Automaton Hierarchy},
|
|
booktitle = {Proceedings of the 8th International Conference on Logic
|
|
for Programming, Artificial Intelligence and Reasoning},
|
|
pages = {39--54},
|
|
year = {2001},
|
|
volume = {2250},
|
|
series = {Lecture Notes in Artificial Intelligence},
|
|
address = {Havana, Cuba},
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
@InProceedings{ somenzi.00.cav,
|
|
author = {Fabio Somenzi and Roderick Bloem},
|
|
title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
|
|
booktitle = {Proceedings of the 12th International Conference on
|
|
Computer Aided Verification (CAV'00)},
|
|
pages = {247--263},
|
|
year = {2000},
|
|
volume = {1855},
|
|
series = {Lecture Notes in Computer Science},
|
|
address = {Chicago, Illinois, USA},
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
@TechReport{ tauriainen.03.a83,
|
|
author = {Heikki Tauriainen},
|
|
title = {On Translating Linear Temporal Logic into Alternating and
|
|
Nondeterministic Automata},
|
|
institution = {Helsinki University of Technology, Laboratory for
|
|
Theoretical Computer Science},
|
|
address = {Espoo, Finland},
|
|
month = dec,
|
|
number = {A83},
|
|
pages = {132},
|
|
type = {Research Report},
|
|
year = {2003},
|
|
note = {Reprint of Licentiate's thesis}
|
|
}
|