MONA IMPLEMENTATION SECRETS

DOI10.1142/S012905410200128XzbMATH Open1066.68079OpenAlexW1987469449MaRDI QIDQ3021971FDOQ3021971

Authors: Nils Klarlund, Anders Møller, Michael I. Schwartzbach 

Publication date: 22 June 2005

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1142/s012905410200128x

Recommendations

• scientific article; zbMATH DE number 1773084
• scientific article; zbMATH DE number 1223628
• Lazy automata techniques for WS1S
• Nested antichains for WS1S
• Nested antichains for WS1S

zbMATH Keywords

finite-state automatamonadic second-order logicMONA tool

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Graph-Based Algorithms for Boolean Function Manipulation
• Weak Second‐Order Arithmetic and Finite Automata
• Tree acceptors and some of their applications
• An nlogn Algorithm for Online BDD Refinement

Cited In (28)

• Bounded treewidth as a key to tractability of knowledge representation and reasoning
• First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
• Nested antichains for WS1S
• Nested antichains for WS1S
• An Evaluation of Automata Algorithms for String Analysis
• Language-Based Abstraction Refinement for Hybrid System Verification
• A symbolic decision procedure for symbolic alternating finite automata
• Deciding monadic second order logic over \(\omega \)-words by specialized finite automata
• Certifying proofs in the first-order theory of rewriting
• Ehrenfeucht-Fraïssé goes automatic for real addition
• Don't care words with an application to the automata-based approach for real addition
• Monitoring metric first-order temporal properties
• Title not available (Why is that?)
• MONA
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic
• Deciding Boolean algebra with Presburger arithmetic
• Title not available (Why is that?)
• Symbolic tree automata
• Automata-based symbolic string analysis for vulnerability detection
• Logic programming approach to automata-based decision procedures
• Turning decision procedures into disprovers
• Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
• Title not available (Why is that?)
• Relativizations for the logic-automata connection
• Lazy automata techniques for WS1S
• Minimization of visibly pushdown automata using partial Max-SAT

This page was built for publication: MONA IMPLEMENTATION SECRETS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3021971)