Abstract
With LoLA, we put recently developed state space oriented algorithms to other tool developers disposal. Providing a simple interface was a major design goal such that it is as easy as possible to integrate LoLA into tools of different application domains. LoLA supports place/transition nets. Implemented verification techniques cover standard properties (liveness, reversibility, boundedness, reachability, dead transitions, deadlocks, home states) as well as satisfiability of state predicates and CTL model checking. For satisfiability, both exhaustive search and heuristically goal oriented system execution are supported. For state space reduction, LoLA features symmetries, stubborn sets, and coverability graphs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Finkel. A minimal coverability graph for Petri nets. Proc. 11th International Conference on Application and Theory of Petri nets, pages 1–21, 1990.
R. Gerth, R. Kuiper, D. Peled, and W. Penczek. A partial order approach to branching time logic model checking. 3rd Israel Symp. on the Theory of Computing and Systems, IEEE 1995, pages 130–140, 1995.
R. M. Karp and R. E. Miller. Parallel programm schemata. Journ. Computer and System Sciences 4, pages 147–195, 1969.
K. Schmidt. Symmetries of Petri nets. Informatik-Bericht 33, Humboldt-Universität zu Berlin, 1994.
K. Schmidt. How to calculate symmetries of Petri nets. Acta Informatica 36, pages 545–590, 2000.
K. Schmidt. Integrating low level symmetries into reachability analysis. Proc. 6th International Conference Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785, pages 315–330, 2000.
K. Schmidt. Stubborn sets for model checking the EF/AG fragment of CTL. to appear in Fundamenta Informaticae, 2000.
K. Schmidt. Stubborn sets for standard properties. 20th International Conference on Application and Theory of Petri nets, LNCS 1639, pages 46–65, 1999.
A. Valmari. Error detection by reduced reachability graph generation. Proc. 9th European Workshop on Application and Theory of Petri Nets, 1988.
A. Valmari. State of the art report: Stubborn sets. Petri net Newsletter 46, pages 6–14, 1994.
B. Vergauwen and J. Lewi. A linear local model checking algorithm for ctl. Proc. CONCUR, LNCS 715, pages 447–461, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt, K. (2000). LoLA A Low Level Analyser. In: Nielsen, M., Simpson, D. (eds) Application and Theory of Petri Nets 2000. ICATPN 2000. Lecture Notes in Computer Science, vol 1825. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44988-4_27
Download citation
DOI: https://doi.org/10.1007/3-540-44988-4_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67693-5
Online ISBN: 978-3-540-44988-1
eBook Packages: Springer Book Archive