768 lines
24 KiB
BibTeX
768 lines
24 KiB
BibTeX
@InProceedings{ babiak.12.tacas,
|
|
author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r
|
|
K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}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{ babiak.13.spin,
|
|
author = {Tom{\'a}{\v{s}} Babiak and Thomas Badie and Alexandre
|
|
Duret-Lutz and Mojm{\'i}r K{\v{r}}et{\'i}nsk{\'y} and Jan
|
|
Strej{\v{c}}ek},
|
|
title = {Compositional Approach to Suspension and Other
|
|
Improvements to {LTL} Translation},
|
|
booktitle = {Proceedings of the 20th International SPIN Symposium on
|
|
Model Checking of Software (SPIN'13)},
|
|
year = 2013,
|
|
volume = {7976},
|
|
series = {Lecture Notes in Computer Science},
|
|
pages = {81--98},
|
|
month = jul,
|
|
publisher = {Springer},
|
|
doi = {10.1007/978-3-642-39176-7_6}
|
|
}
|
|
|
|
@InProceedings{ baier.19.atva,
|
|
author = {Christel Baier and Franti\v{s}ek Blahoudek and Alexandre
|
|
Duret-Lutz and Joachim Klein and David M\"uller and Jan
|
|
Strej\v{c}ek},
|
|
title = {Generic Emptiness Check for Fun and Profit},
|
|
booktitle = {Proceedings of the 17th International Symposium on
|
|
Automated Technology for Verification and Analysis
|
|
(ATVA'19)},
|
|
year = {2019},
|
|
volume = {?????},
|
|
series = {Lecture Notes in Computer Science},
|
|
pages = {???--???},
|
|
month = oct,
|
|
publisher = {Springer},
|
|
note = {To appear}
|
|
}
|
|
|
|
@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
|
|
}
|
|
|
|
@InProceedings{ benedikt.13.tacas,
|
|
author = {Michael Benedikt and Rastislav Lenhardt and James
|
|
Worrell},
|
|
title = {{LTL} Model Checking of Interval Markov Chains},
|
|
booktitle = {19th International Conference on Tools and Algorithms for
|
|
the Construction and Analysis of Systems (TACAS'13)},
|
|
year = {2013},
|
|
pages = {32--46},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = {7795},
|
|
editor = {Nir Piterman and Scott A. Smolka},
|
|
publisher = {Springer}
|
|
}
|
|
|
|
@Article{ boker.2011.fossacs,
|
|
author = {Udi Boker and Orna Kupferman},
|
|
title = {Co-Büching Them All},
|
|
booktitle = {Foundations of Software Science and Computational
|
|
Structures - 14th International Conference, FOSSACS 2011},
|
|
year = {2011},
|
|
pages = {184--198},
|
|
url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
|
|
}
|
|
|
|
@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}
|
|
}
|
|
|
|
@Article{ carton.99.ita,
|
|
author = {Olivier Carton and Ram{\'o}n Maceiras},
|
|
title = {Computing the {R}abin index of a parity automaton},
|
|
journal = {Informatique théorique et applications},
|
|
year = {1999},
|
|
volume = {33},
|
|
number = {6},
|
|
pages = {495--505}
|
|
}
|
|
|
|
@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}
|
|
}
|
|
|
|
@InProceedings{ cichon.09.depcos,
|
|
author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski},
|
|
title = {Minimal {B\"uchi} Automata for Certain Classes of {LTL}
|
|
Formulas},
|
|
booktitle = {Proceedings of the Fourth International Conference on
|
|
Dependability of Computer Systems},
|
|
pages = {17--24},
|
|
year = 2009,
|
|
publisher = {IEEE Computer Society}
|
|
}
|
|
|
|
@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/}}
|
|
}
|
|
|
|
@Article{ courcoubetis.92.fmsd,
|
|
author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre Wolper
|
|
and Mihalis Yannakakis},
|
|
title = {Memory-Efficient Algorithm for the Verification of
|
|
Temporal Properties},
|
|
journal = {Formal Methods in System Design},
|
|
pages = {275--288},
|
|
year = {1992},
|
|
volume = {1}
|
|
}
|
|
|
|
@InProceedings{ couvreur.99.fm,
|
|
author = {Jean-Michel Couvreur},
|
|
title = {On-the-fly Verification of Temporal Logic},
|
|
pages = {253--271},
|
|
editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
|
|
booktitle = {Proceedings of the World Congress on Formal Methods in the
|
|
Development of Computing Systems (FM'99)},
|
|
publisher = {Springer-Verlag},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = {1708},
|
|
year = {1999},
|
|
month = sep,
|
|
isbn = {3-540-66587-0}
|
|
}
|
|
|
|
@InProceedings{ dax.07.atva,
|
|
author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
|
|
title = {Mechanizing the Powerset Construction for Restricted
|
|
Classes of {$\omega$}-Automata},
|
|
year = 2007,
|
|
series = {Lecture Notes in Computer Science},
|
|
publisher = {Springer-Verlag},
|
|
volume = 4762,
|
|
booktitle = {Proceedings of the 5th International Symposium on
|
|
Automated Technology for Verification and Analysis
|
|
(ATVA'07)},
|
|
editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
|
|
and Yoshio Okamura},
|
|
month = oct
|
|
}
|
|
|
|
@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}
|
|
}
|
|
|
|
@Article{ duret.14.ijccbs,
|
|
author = {Alexandre Duret-Lutz},
|
|
title = {{LTL} Translation Improvements in {S}pot 1.0},
|
|
journal = {International Journal on Critical Computer-Based Systems},
|
|
year = {2014},
|
|
volume = {5},
|
|
number = {1/2},
|
|
pages = {31--54},
|
|
month = mar,
|
|
doi = {10.1504/IJCCBS.2014.059594}
|
|
}
|
|
|
|
@InProceedings{ dwyer.98.fmsp,
|
|
author = {Matthew B. Dwyer and George S. Avrunin and James C.
|
|
Corbett},
|
|
title = {Property Specification Patterns for Finite-state
|
|
Verification},
|
|
booktitle = {Proceedings of the 2nd Workshop on Formal Methods in
|
|
Software Practice (FMSP'98)},
|
|
publisher = {ACM Press},
|
|
editor = {Mark Ardis},
|
|
month = mar,
|
|
year = 1998,
|
|
pages = {7--15}
|
|
}
|
|
|
|
@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.}
|
|
}
|
|
|
|
@Article{ etessami.00.ipl,
|
|
author = {Kousha Etessami},
|
|
title = {A note on a question of {P}eled and {W}ilke regarding
|
|
stutter-invariant {LTL}},
|
|
journal = {Information Processing Letters},
|
|
volume = {75},
|
|
number = {6},
|
|
year = {2000},
|
|
pages = {261--263}
|
|
}
|
|
|
|
@InProceedings{ gastin.01.cav,
|
|
author = {Paul Gastin and Denis Oddoux},
|
|
title = {Fast {LTL} to {B\"u}chi Automata Translation},
|
|
booktitle = {Proceedings of the 13th International Conference on
|
|
Computer Aided Verification (CAV'01)},
|
|
pages = {53--65},
|
|
year = 2001,
|
|
editor = {G. Berry and H. Comon and A. Finkel},
|
|
volume = {2102},
|
|
series = {Lecture Notes in Computer Science},
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
@InProceedings{ geldenhuys.04.tacas,
|
|
author = {Jaco Geldenhuys and Antti Valmari},
|
|
title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification
|
|
More Efficient},
|
|
booktitle = {Proceedings of the 10th International Conference on Tools
|
|
and Algorithms for the Construction and Analysis of Systems
|
|
(TACAS'04)},
|
|
editor = {Kurt Jensen and Andreas Podelski},
|
|
pages = {205--219},
|
|
year = {2004},
|
|
publisher = {Springer-Verlag},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = {2988},
|
|
isbn = {3-540-21299-X}
|
|
}
|
|
|
|
@InProceedings{ geldenhuys.06.spin,
|
|
author = {Jaco Geldenhuys and Henri Hansen},
|
|
title = {Larger Automata and Less Work for {LTL} Model Checking},
|
|
booktitle = {Proceedings of the 13th International SPIN Workshop
|
|
(SPIN'06)},
|
|
year = {2006},
|
|
pages = {53--70},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = {3925},
|
|
publisher = {Springer}
|
|
}
|
|
|
|
@TechReport{ holevek.04.tr,
|
|
title = {Verification Results in {Liberouter} Project},
|
|
author = {J. Hole\v{c}ek and T. Kratochv\'ila and V. \v{R}eh\'ak and
|
|
D. \v{S}afr\'anek and P. \v{S}ime\v{c}ek},
|
|
month = {September},
|
|
year = 2004,
|
|
number = 03,
|
|
institution = {CESNET}
|
|
}
|
|
|
|
@Book{ holzmann.91.book,
|
|
author = {Gerard J. Holzmann},
|
|
title = {Design and Validation of Computer Protocols},
|
|
publisher = {Prentice-Hall},
|
|
address = {Englewood Cliffs, New Jersey},
|
|
year = {1991}
|
|
}
|
|
|
|
@InProceedings{ jacobs.16.synt,
|
|
author = {Swen Jacobs and Felix Klein and Sebastian Schirmer},
|
|
title = {A High-Level {LTL} Synthesis Format: {TLSF} v1.1},
|
|
booktitle = {Proceedings Fifth Workshop on Synthesis (SYNT@CAV'16)},
|
|
pages = {112--132},
|
|
year = {2016},
|
|
series = {Electronic Proceedings in Theoretical Computer Science},
|
|
volume = {229},
|
|
doi = {10.4204/EPTCS.229.10}
|
|
}
|
|
|
|
@InProceedings{ kretisnky.12.cav,
|
|
author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza},
|
|
title = {Deterministic Automata for the {(F,G)}-Fragment of {LTL}},
|
|
booktitle = {24th International Conference on Computer Aided
|
|
Verification (CAV'12)},
|
|
year = 2012,
|
|
pages = {7--22},
|
|
doi = {10.1007/978-3-642-31424-7_7},
|
|
url = {https://doi.org/10.1007/978-3-642-31424-7_7},
|
|
isbn = {978-3-642-31424-7},
|
|
publisher = {Springer}
|
|
}
|
|
|
|
@InProceedings{ kuperberg.15.icalp,
|
|
author = {Denis Kuperberg and Micha{\l} Skrzypczak },
|
|
title = {On Determinisation of Good-for-Games Automata},
|
|
booktitle = {Proceedings of the 42nd International Colloquium on
|
|
Automata, Languages, and Programming (ICALP'15)},
|
|
pages = {299--310},
|
|
year = {2015},
|
|
publisher = {Springer},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = 9135,
|
|
doi = {10.1007/978-3-662-47666-6_24}
|
|
}
|
|
|
|
@Article{ kupferman.01.tocl,
|
|
author = {Orna Kupferman and Moshe Y. Vardi},
|
|
title = {Weak alternating automata are not that weak},
|
|
journal = {ACM Transactions on Computational Logic (TOCL)},
|
|
month = {July},
|
|
year = 2001,
|
|
pages = {408--429},
|
|
volume = {2},
|
|
number = {3},
|
|
publisher = {ACM New York, NY, USA}
|
|
}
|
|
|
|
@Article{ kupferman.05.tcl,
|
|
author = {Orna Kupferman and Moshe Y. Vardi},
|
|
title = {From Linear Time to Branching Time},
|
|
journal = {ACM Transactions on Computational Logic},
|
|
volume = {6},
|
|
number = {2},
|
|
month = apr,
|
|
year = {2005},
|
|
pages = {273--294},
|
|
doi = {10.1145/1055686.1055689},
|
|
acmid = {1055689},
|
|
publisher = {ACM}
|
|
}
|
|
|
|
@Article{ kupferman.05.tcs,
|
|
author = {Orna Kupferman and Moshe Y. Vardi},
|
|
title = {From complementation to certification},
|
|
journal = {Theoretical Computer Science},
|
|
month = {November},
|
|
year = 2005,
|
|
pages = {83--100},
|
|
volume = {345},
|
|
number = {1},
|
|
publisher = {Elsevier}
|
|
}
|
|
|
|
@InProceedings{ kupferman.10.mochart,
|
|
author = {Orna Kupferman and Adin Rosenberg},
|
|
title = {The Blow-Up in Translating {LTL} do Deterministic
|
|
Automata},
|
|
booktitle = {Proceedings of the 6th International Workshop on Model
|
|
Checking and Artificial Intelligence (MoChArt 2010)},
|
|
pages = {85--94},
|
|
year = 2011,
|
|
volume = {6572},
|
|
series = {Lecture Notes in Artificial Intelligence},
|
|
month = nov,
|
|
publisher = {Springer},
|
|
note = {See also
|
|
\url{https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf}}
|
|
}
|
|
|
|
@MastersThesis{ loding.98.msc,
|
|
author = {Christof Löding},
|
|
title = {Methods for the Transformation of ω-Automata: Complexity
|
|
and Connection to Second Order Logic},
|
|
school = {Institute of Computer Science and Applied Mathematics
|
|
Christian-Albrechts-University of Kiel},
|
|
year = {1998}
|
|
}
|
|
|
|
@InProceedings{ loding.99.fstts,
|
|
author = {Christof L{\"o}ding},
|
|
title = {Optimal Bounds for Transformations of {$\omega$}-Automata},
|
|
booktitle = {Proceedings of the 19th Conference on Foundations of
|
|
Software Technology and Theoretical Computer Science
|
|
(FSTTCS'99)},
|
|
year = 1999,
|
|
publisher = {Springer},
|
|
pages = {97--109},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = 1738,
|
|
doi = {10.1007/3-540-46691-6_8}
|
|
}
|
|
|
|
@Article{ loizou.82.is,
|
|
author = {George Loizou and Peter Thanisch},
|
|
title = {Enumerating the Cycles of a Digraph: A New Preprocessing
|
|
Strategy},
|
|
journal = {Information Sciences},
|
|
year = {1982},
|
|
volume = {27},
|
|
number = {3},
|
|
pages = {163--182},
|
|
month = aug
|
|
}
|
|
|
|
@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}
|
|
}
|
|
|
|
@InProceedings{ michaud.15.spin,
|
|
author = {Thibaud Michaud and Alexandre Duret-Lutz},
|
|
title = {Practical Stutter-Invariance Checks for {$\omega$}-Regular
|
|
Languages},
|
|
booktitle = {Proceedings of the 22th International SPIN Symposium on
|
|
Model Checking of Software (SPIN'15)},
|
|
year = 2015,
|
|
pages = {84--101},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = 9232,
|
|
publisher = {Springer},
|
|
month = aug
|
|
}
|
|
|
|
@InProceedings{ minato.92.sasimi,
|
|
author = {Shin-ichi Minato},
|
|
title = {Fast Generation of Irredundant Sum-of-Products Forms from
|
|
Binary Decision Diagrams},
|
|
booktitle = {Proceedings of the third Synthesis and Simulation and
|
|
Meeting International Interchange workshop (SASIMI'92)},
|
|
pages = {64--73},
|
|
year = {1992},
|
|
address = {Kobe, Japan},
|
|
month = {April}
|
|
}
|
|
|
|
@InProceedings{ muller.17.gandalf,
|
|
author = {David M\"uller and Salomon Sickert},
|
|
title = {{LTL} to Deterministic {E}merson-{L}ei Automata},
|
|
booktitle = {Proceedings of the 8th International Sumposium on Games,
|
|
Automata, Logics and Formal Verification (GandALF'17)},
|
|
year = 2017,
|
|
publisher = {Open Publishing Association},
|
|
series = {Electronic Proceedings in Theoretical Computer Science},
|
|
volume = {256},
|
|
pages = {180--194},
|
|
doi = {10.4204/EPTCS.256.13}
|
|
}
|
|
|
|
@InProceedings{ pelanek.07.spin,
|
|
author = {Radek Pel\'{a}nek},
|
|
title = {{BEEM}: benchmarks for explicit model checkers},
|
|
booktitle = {Proceedings of the 14th international SPIN conference on
|
|
Model checking software},
|
|
year = 2007,
|
|
pages = {263--267},
|
|
numpages = {5},
|
|
volume = {4595},
|
|
series = {Lecture Notes in Computer Science},
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
@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{ renault.13.tacas,
|
|
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
|
|
Kordon and Denis Poitrenaud},
|
|
title = {Strength-Based Decomposition of the Property {B\"u}chi
|
|
Automaton for Faster Model Checking},
|
|
booktitle = {Proceedings of the 19th International Conference on Tools
|
|
and Algorithms for the Construction and Analysis of Systems
|
|
(TACAS'13)},
|
|
year = {2013},
|
|
pages = {580--593},
|
|
publisher = {Springer},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = {7795},
|
|
doi = {10.1007/978-3-642-36742-7_42}
|
|
}
|
|
|
|
@InProceedings{ rozier.07.spin,
|
|
author = {Kristin Y. Rozier and Moshe Y. Vardi},
|
|
title = {LTL Satisfiability Checking},
|
|
booktitle = {Proceedings of the 12th International SPIN Workshop on
|
|
Model Checking of Software (SPIN'07)},
|
|
pages = {149--167},
|
|
year = 2007,
|
|
volume = {4595},
|
|
series = {Lecture Notes in Computer Science},
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
@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}
|
|
}
|
|
|
|
@TechReport{ schwoon.04.tr,
|
|
author = {Stefan Schwoon and Javier Esparza},
|
|
institution = {Universit{\"a}t Stuttgart, Fakult\"at Informatik,
|
|
Elektrotechnik und Informationstechnik},
|
|
month = {November},
|
|
number = {2004/06},
|
|
title = {A Note on On-The-Fly Verification Algorithms},
|
|
year = {2004},
|
|
url = {http://www.fmi.uni-stuttgart.de/szs/publications/info/schwoosn.SE04.shtml}
|
|
}
|
|
|
|
@InProceedings{ sebastiani.03.charme,
|
|
author = {Roberto Sebastiani and Stefano Tonetta},
|
|
title = {"More Deterministic" vs. "Smaller" B{\"u}chi Automata for
|
|
Efficient LTL Model Checking},
|
|
booktitle = {Proceedings for the 12th Advanced Research Working
|
|
Conference on Correct Hardware Design and Verification
|
|
Methods (CHARME'03)},
|
|
pages = {126--140},
|
|
year = {2003},
|
|
editor = {G. Goos and J. Hartmanis and J. van Leeuwen},
|
|
volume = {2860},
|
|
series = {Lectures Notes in Computer Science},
|
|
month = {October},
|
|
publisher = {Springer-Verlag}
|
|
}
|
|
|
|
@InProceedings{ sickert.16.cav,
|
|
author = {Salomon Sickert and Javier Esparza and Stefaan Jaax and
|
|
Jan K{\v{r}}et{\'i}nsk{\'y}},
|
|
title = {Limit-Deterministic {B\"u}chi Automata for Linear Temporal
|
|
Logic},
|
|
booktitle = {Proceedings of the 28th International Conference on
|
|
Computer Aided Verification (CAV'16)},
|
|
year = 2016,
|
|
publisher = {Springer-Verlag},
|
|
series = {Lecture Notes in Computer Science},
|
|
volume = {9780},
|
|
pages = {312--332},
|
|
doi = {10.1007/978-3-319-41540-6_17}
|
|
}
|
|
|
|
@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}
|
|
}
|
|
|
|
@Book{ systemverilog.18.std,
|
|
title = {1800-2017 - IEEE Standard for SystemVerilog--Unified
|
|
Hardware Design, Specification, and Verification Language},
|
|
publisher = {IEEE},
|
|
year = {2018},
|
|
month = feb,
|
|
doi = {10.1109/IEEESTD.2018.8299595}
|
|
}
|
|
|
|
@InProceedings{ tabakov.10.rv,
|
|
author = {Deian Tabakov and Moshe Y. Vardi},
|
|
title = {Optimized Temporal Monitors for {SystemC}},
|
|
booktitle = {Proceedings of the 1st International Conference on Runtime
|
|
Verification (RV'10)},
|
|
pages = {436--451},
|
|
year = 2010,
|
|
volume = {6418},
|
|
series = {Lecture Notes in Computer Science},
|
|
month = nov,
|
|
publisher = {Springer}
|
|
}
|
|
|
|
@TechReport{ tauriainen.00.tr,
|
|
author = {Heikki Tauriainen},
|
|
title = {Automated Testing of {B\"u}chi Automata Translators for
|
|
{L}inear {T}emporal {L}ogic},
|
|
address = {Espoo, Finland},
|
|
institution = {Helsinki University of Technology, Laboratory for
|
|
Theoretical Computer Science},
|
|
number = {A66},
|
|
year = {2000},
|
|
type = {Research Report},
|
|
note = {Reprint of Master's thesis}
|
|
}
|
|
|
|
@TechReport{ tauriainen.03.tr,
|
|
address = {Espoo, Finland},
|
|
author = {Heikki Tauriainen},
|
|
institution = {Helsinki University of Technology, Laboratory for
|
|
Theoretical Computer Science},
|
|
month = {December},
|
|
number = {A83},
|
|
pages = {132},
|
|
title = {On Translating Linear Temporal Logic into Alternating and
|
|
Nondeterministic Automata},
|
|
type = {Research Report},
|
|
year = {2003},
|
|
note = {Reprint of Licentiate's thesis}
|
|
}
|
|
|
|
@TechReport{ tauriainen.06.tr,
|
|
address = {Espoo, Finland},
|
|
author = {Heikki Tauriainen},
|
|
month = {September},
|
|
note = {Doctoral dissertation},
|
|
number = {A104},
|
|
title = {Automata and Linear Temporal Logic: Translations with
|
|
Transition-Based Acceptance},
|
|
type = {Research Report},
|
|
year = {2006}
|
|
}
|
|
|
|
@InProceedings{ thirioux.02.fmics,
|
|
author = {Xavier Thirioux},
|
|
title = {Simple and Efficient Translation from {LTL} Formulas to
|
|
{B\"u}chi Automata},
|
|
booktitle = {Proceedings of the 7th International ERCIM Workshop in
|
|
Formal Methods for Industrial Critical Systems (FMICS'02)},
|
|
series = {Electronic Notes in Theoretical Computer Science},
|
|
volume = {66(2)},
|
|
publisher = {Elsevier},
|
|
editor = {Rance Cleaveland and Hubert Garavel},
|
|
year = {2002},
|
|
month = jul,
|
|
address = {M{\'a}laga, Spain}
|
|
}
|
|
|
|
@InBook{ thomas.97.chapter,
|
|
author = {Wolfgang Thomas},
|
|
title = {Languages, Automata, and Logic},
|
|
booktitle = {Handbook of Formal Languages --- Volume 3 Beyond Words},
|
|
editor = {Grzegorz Rozenberg and Arto Salomaa},
|
|
chapter = 7,
|
|
publisher = {Springer-Verlag},
|
|
year = {1997}
|
|
}
|
|
|
|
@Article{ zielonka.98.tcs,
|
|
author = {Wieslaw Zielonka},
|
|
title = {Infinite games on finitely coloured graphs with
|
|
applications to automata on infinite trees},
|
|
journal = {Theoretical Computer Science},
|
|
volume = {200},
|
|
number = {1},
|
|
pages = {135--183},
|
|
year = {1998}
|
|
}
|