A decidability result for the model checking of infinite-state systems
From MaRDI portal
Publication:438572
DOI10.1007/s10817-010-9192-zzbMath1279.68226OpenAlexW2015063037MaRDI QIDQ438572
Enrica Nicolini, Daniele Zucchelli
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9192-z
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)
Uses Software
Cites Work
- Model-theoretic methods in combined constraint satisfiability
- Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
- On the interpretability of arithmetic in temporal logic
- Concerning the semantic consequence relation in first-order temporal logic
- A decision procedure for combinations of propositional temporal logic and other specialized theories
- The power of temporal proofs
- Incompleteness of first-order temporal logic with until
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Towards a Model-Checker for Counter Systems
- Noetherianity and Combination Problems
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Interpolation in Local Theory Extensions
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Linear-time temporal logics with Presburger constraints: an overview ★
- Simplification by Cooperating Decision Procedures
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- Decidability and incompleteness results for first-order temporal logics of linear time
- Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
- Tools and Algorithms for the Construction and Analysis of Systems
- Perspectives of System Informatics
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A decidability result for the model checking of infinite-state systems
