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

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)

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

Cites work

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

Cited in

(28)

• Automata-based symbolic string analysis for vulnerability detection
• scientific article; zbMATH DE number 1670771 (Why is no real title available?)
• An Evaluation of Automata Algorithms for String Analysis
• scientific article; zbMATH DE number 2102722 (Why is no real title available?)
• Nested antichains for WS1S
• Nested antichains for WS1S
• Ehrenfeucht-Fraïssé goes automatic for real addition
• Monitoring metric first-order temporal properties
• Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
• Bounded treewidth as a key to tractability of knowledge representation and reasoning
• Logic programming approach to automata-based decision procedures
• Relativizations for the logic-automata connection
• Certifying proofs in the first-order theory of rewriting
• Turning decision procedures into disprovers
• MONA
• Don't care words with an application to the automata-based approach for real addition
• Language-Based Abstraction Refinement for Hybrid System Verification
• A symbolic decision procedure for symbolic alternating finite automata
• Lazy automata techniques for WS1S
• Minimization of visibly pushdown automata using partial Max-SAT
• scientific article; zbMATH DE number 1773084 (Why is no real title available?)
• First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
• Symbolic tree automata
• Deciding monadic second order logic over \(\omega \)-words by specialized finite automata
• 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

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)