A decidability result for the model checking of infinite-state systems
type: Item
instance of: scholarly article
title: A decidability result for the model checking of infinite-state systems
zbMATH Open document ID: 1279.68226
author: Daniele Zucchelli
author: Enrica Nicolini
published in: Journal of Automated Reasoning
publication date: 2012-07-31T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 6062062
zbMATH Keywords: model checking
zbMATH Keywords: combination methods
zbMATH Keywords: satisfiability problems
zbMATH Keywords: infinite-state systems
describes a project that uses: NuSMV
MaRDI profile type: Publication
full work available at URL: s10817-010-9192-z
OpenAlex ID: W2015063037
cites work: The power of temporal proofs
cites work: Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
cites work: Q2754102
cites work: Q4804909
cites work: Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
cites work: Towards a Model-Checker for Counter Systems
cites work: Linear-time temporal logics with Presburger constraints: an overview ★
cites work: Q4809077
cites work: Q4298571
cites work: Model-theoretic methods in combined constraint satisfiability
cites work: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
cites work: Noetherianity and Combination Problems
cites work: Q4003410
cites work: On the interpretability of arithmetic in temporal logic
cites work: Q4551161
cites work: Q4873991
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Decidability and incompleteness results for first-order temporal logics of linear time
cites work: Recursive unsolvability of Post's problem of ''Tag'' und other topics in theory of Turing machines
cites work: Simplification by Cooperating Decision Procedures
cites work: On an interpretation of second order quantification in first order intuitionistic propositional logic
cites work: A decision procedure for combinations of propositional temporal logic and other specialized theories
cites work: Perspectives of System Informatics
cites work: Interpolation in Local Theory Extensions
cites work: Concerning the semantic consequence relation in first-order temporal logic
cites work: Incompleteness of first-order temporal logic with until
cites work: Q4385439
cites work: Unions of non-disjoint theories and combinations of satisfiability procedures
cites work: Q4893140
DOI: 10.1007/S10817-010-9192-Z
description: scientific article; zbMATH DE number 6062062