Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols

DOI10.1016/S1571-0661(04)00186-0zbMath1262.68039MaRDI QIDQ4921500

Vlad Rusu, Elena Zinovieva

Publication date: 10 May 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• PVS
• CADP
• Omega
• ICS

Cites Work

• Unnamed Item
• Symbolic model checking: \(10^{20}\) states and beyond
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• Solvable cases of the decision problem
• A Practical Decision Procedure for Arithmetic with Function Symbols
• Presburger arithmetic with unary predicates is Π₁¹ complete
• Selecting Software Test Data Using Data Flow Information

This page was built for publication: Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols