LoLa: A low level analyser. 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

References in zbMATH (referenced in 19 articles )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Dong, Jin Song; Liu, Yang; Sun, Jun; Zhang, Xian: Towards verification of computation orchestration (2014)
  2. Evangelista, Sami; Kristensen, Lars Michael: Hybrid on-the-fly LTL model checking with the sweep-line method (2012)
  3. Jensen, Kurt; Kristensen, Lars M.; Mailund, Thomas: The sweep-line state space exploration method (2012)
  4. Lapadula, A.; Pugliese, R.; Tiezzi, F.: A WSDL-based type system for asynchronous WS-BPEL processes (2011)
  5. Kristensen, L.M.; Schmidt, K.; Valmari, A.: Question-guided stubborn set methods for state properties (2006)
  6. Schmidt, Karsten: Automated generation of a progress measure for the sweep-line method (2006)
  7. Comet, Jean-Paul; Klaudel, Hanna; Liauzu, Stéphane: Modeling multi-valued genetic regulatory networks using high-level Petri nets (2005)
  8. Reisig, Wolfgang; Schmidt, Karsten; Stahl, Christian: Kommunizierende Workflow-services modellieren und analysieren (2005)
  9. Junttila, Tommi A.: New canonical representative marking algorithms for place/transition-nets (2004)
  10. Kristensen, Lars Michael; Christensen, Søren: Implementing coloured Petri nets using a functional programming language (2004)
  11. Schmidt, Karsten: Automated generation of a progress measure for the sweep-line method (2004)
  12. Dehnert, Juliane: Four steps towards sound business process models (2003)
  13. Schmidt, Karsten: Using Petri net invariants in state space construction (2003)
  14. Dehnert, Juliane: Non-controllable choice robustness expressing the controllability of workflow processes (2002)
  15. Mäkelä, Marko: Maria: Modular reachability analyser for algebraic system nets (2002)
  16. Latvala, Timo: Model checking LTL properties of high-level Petri nets with fairness constraints (2001)
  17. Mäkelä, Marko: Optimising enabling tests and unfoldings of algebraic system nets (2001)
  18. Schmidt, Karsten: Narrowing Petri net state spaces using the state equation (2001)
  19. Schmidt, Karsten: LoLa: A low level analyser (2000)