Next: , Previous: Interfacing with lbtt, Up: Top


References

[CGP99]
E. Clarke Jr., O. Grumberg and D. Peled. Model checking. The MIT Press, 1999.
[Cou99]
J.-M. Couvreur. On-the-fly verification of linear temporal logic. In Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM'99), volume I, volume 1708 of Lecture Notes in Computer Science, pages 253—271. Springer-Verlag, 1999.
[DGV99]
M. Daniele, F. Giunchiglia and M. Y. Vardi. Improved automata generation for linear temporal logic. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99), volume 1633 of Lecture Notes in Computer Science, pages 249—260. Springer-Verlag, 1999.
[DP04]
A. Duret-Lutz and D. Poitrenaud. SPOT: An Extensible Model Checking Library Using Transition-Based Generalized Büchi Automata. In Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2004), pages 76–83. IEEE Computer Society Press, 2004.
[EH00]
K. Etessami and G. Holzmann. Optimizing Büchi automata. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000), volume 1877 of Lecture Notes in Computer Science, pages 153—167. Springer-Verlag, 2000.
[Ete99]
K. Etessami. Stutter-invariant languages, omega-automata, and temporal logic. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99), volume 1633 of Lecture Notes in Computer Science, pages 236—248. Springer-Verlag, 1999.
[Ete02]
K. Etessami. A hierarchy of polynomial-time computable simulations for automata. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR 2002), volume 2421 of Lecture Notes in Computer Science, pages 131—144. Springer-Verlag, 2002.
[EWS01]
K. Etessami, Th. Wilke and R. Schuller. Fair simulation relations, parity games, and state space reduction for Büchi automata. In Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP 2001), volume 2076 of Lecture Notes in Computer Science, pages 694—707. Springer-Verlag, 2001.
[Fri03]
C. Fritz. Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. In Proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA 2003), volume 2759 of Lecture Notes in Computer Science, pages 35—48. Springer-Verlag, 2003.
[GO01]
P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV 2001), volume 2102 of Lecture Notes in Computer Science, pages 53—65. Springer-Verlag, 2001.
[GO03]
P. Gastin and D. Oddoux. LTL with past and two-way weak alternating automata. In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS 2003), volume 2747 of Lecture Notes in Computer Science, pages 439—448. Springer-Verlag, 2003.
[Gei01]
M. C. W. Geilen. On the construction of monitors for temporal logic properties. Electronic Notes for Theoretical Computer Science, 55(2), 2001.
[GPVW95]
R. Gerth, D. Peled, M. Y. Vardi and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing, and Verification (PSTV'95), pages 3—18. Chapman & Hall, 1995.
[GL02]
D. Giannakopoulou and F. Lerda. From states to transitions: Improving translation of LTL formulae to Büchi automata. In Proceedings of the 22nd IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002), volume 2529 of Lecture Notes in Computer Science, pages 308—326. Springer-Verlag, 2002.
[GSB02]
S. Gurumurthy, F. Somenzi and R. Bloem. Fair simulation minimization. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002), volume 2404 of Lecture Notes in Computer Science, pages 610—624. Springer-Verlag, 2002.
[GViz]
GraphViz - open source graph drawing software. See <http://www.research.att.com/sw/tools/graphviz/>.
[Hol97]
G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279—295, 1997.
[Isl94]
A. Isli. Mapping an LPTL formula into a Büchi alternating automaton accepting its models. In Temporal Logic: Proceedings of the ICTL Workshop, pages 85—90. Research Report MPI-I-94-230, Max-Planck-Institut für Informatik, 1994.
[Lat03]
T. Latvala. Efficient model checking of safety properties. In Proceedings of the 10th Spin Workshop on Model Checking of Software (SPIN 2003), volume 2648 of Lecture Notes in Computer Science, pages 74—88. Springer-Verlag, 2003.
[Sch01]
K. Schneider. Improving automata generation for linear temporal logic by considering the automaton hierarchy. In Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2001), volume 2250 of Lecture Notes in Computer Science, pages 39—54. Springer-Verlag, 2001.
[ST03]
R. Sebastiani and S. Tonetta. “More deterministic” vs. “smaller” Büchi automata for efficient LTL model checking. In Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2003), volume 2860 of Lecture Notes in Computer Science, pages 126—140. Springer-Verlag, 2003.
[SB00]
F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV 2000), volume 1855 of Lecture Notes in Computer Science, pages 247—263. Springer-Verlag, 2000.
[Tau00]
H. Tauriainen. Automated testing of Büchi automata translators for linear temporal logic. Research report A66, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, 2000. Available on the WWW at <http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A66.shtml>.
[TH02]
H. Tauriainen and K. Heljanko. Testing LTL formula translation into Büchi automata. International Journal on Software Tools for Technology Transfer (STTT) 4(1):57—70, 2002.
[Thi02]
X. Thirioux. Simple and efficient translation from LTL formulas to B"uchi automata. Electronic Notes in Theoretical Computer Science, 66(2), 2002.
[Var96]
M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, volume 1043 of Lecture Notes in Computer Science, pages 238—265. Springer-Verlag, 1996.
[VW86]
M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First IEEE Symposium on Logic in Computer Science (LICS'86), pages 332—344. IEEE Computer Society Press, 1986.
[Wol01]
P. Wolper. Constructing automata from temporal logic formulas: A tutorial. In Lectures on Formal Methods and Performance Analysis: First EEF/Euro Summer School on Trends in Computer Science, Revised Lectures, volume 2090 of Lecture Notes in Computer Science, pages 261—277. Springer-Verlag, 2001.