MONA IMPLEMENTATION SECRETS

DOI10.1142/S012905410200128XMaRDI QIDQ3021971zbMATH OpenOpenAlexFDO

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 automataMONA toolmonadic second-order logic

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

(32)

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