MONA

MONA implementation secrets. The MONA tool provides an implementation of automaton-based decision procedures for the logics WS1S and WS2S. It has been used for numerous applications, and it is remarkably efficient in practice, even though it faces a theoretically non-elementary worst-case complexity. The implementation has matured over a period of six years. Compared to the first naive version, the present tool is faster by several orders of magnitude. This speedup is obtained from many different contributions working on all levels of the compilation and execution of formulas. We present an overview of MONA and a selection of implementation “secrets” that have been discovered and tested over the years, including formula reductions, DAGification, guided tree automata, three-valued logic, eager minimization, BDD-based automata representations, and cache-conscious data structures. We describe these techniques and quantify their respective effects by experimenting with separate versions of the MONA tool that in turn omit each of them.


References in zbMATH (referenced in 135 articles , 2 standard articles )

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

1 2 3 ... 5 6 7 next

  1. Pandya, Paritosh K.; Wakankar, Amol: Specification and optimal reactive synthesis of run-time enforcement shields (2022)
  2. Esparza, Javier; Raskin, Mikhail; Welzel, Christoph: Computing parameterized invariants of parameterized Petri nets (2021)
  3. Havlena, Vojtěch; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Automata terms in a lazy (\mathrmWSk\mathrmS) decision procedure (2021)
  4. Löding, Christof; Thomas, Wolfgang: Automata on finite trees (2021)
  5. Havelund, Klaus; Peled, Doron; Ulus, Dogan: First-order temporal logic monitoring with BDDs (2020)
  6. Im, Hyeonseung; Genevès, Pierre; Gesbert, Nils; Layaïda, Nabil: Backward type inference for XML queries (2020)
  7. Landwehr, Patrick; Löding, Christof: Projection for Büchi tree automata with constraints between siblings (2020)
  8. Tabajara, Lucas M.; Vardi, Moshe Y.: LTLf synthesis under partial observability: from theory to practice (2020)
  9. Wells, Andrew M.; Lahijanian, Morteza; Kavraki, Lydia E.; Vardi, Moshe Y.: (\mathrmLTL_f) synthesis on probabilistic systems (2020)
  10. Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Nested antichains for WS1S (2019)
  11. Havlena, Vojtěch; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Automata terms in a lazy (\mathrmWSk\mathrmS) decision procedure (2019)
  12. Pandya, Paritosh K.; Wakankar, Amol: Specification and optimal reactive synthesis of run-time enforcement shields (2019)
  13. Abdulla, Parosh Aziz; Sistla, A. Prasad; Talupur, Muralidhar: Model checking parameterized systems (2018)
  14. Aiswarya, C.; Bollig, Benedikt; Gastin, Paul: An automata-theoretic approach to the verification of distributed algorithms (2018)
  15. Avni, Guy; Kupferman, Orna: Synthesis from component libraries with costs (2018)
  16. Dahlberg, Axel; Wehner, Stephanie: Transforming graph states using single-qubit operations (2018)
  17. D’Antoni, Loris; Kincaid, Zachary; Wang, Fang: A symbolic decision procedure for symbolic alternating finite automata (2018)
  18. Mandrioli, Dino; Pradella, Matteo: Generalizing input-driven languages: theoretical and practical benefits (2018)
  19. Feldman, Yotam M. Y.; Padon, Oded; Immerman, Neil; Sagiv, Mooly; Shoham, Sharon: Bounded quantifier instantiation for checking inductive invariants (2017)
  20. Fiedor, Tomáš; Holík, Lukáš; Janků, Petr; Lengál, Ondřej; Vojnar, Tomáš: Lazy automata techniques for WS1S (2017)

1 2 3 ... 5 6 7 next


Further publications can be found at: http://www.brics.dk/mona/publications.html