Computable fixpoints in well-structured symbolic model checking
From MaRDI portal
Publication:2248074
DOI10.1007/s10703-012-0168-yzbMath1291.68247OpenAlexW1988270822MaRDI QIDQ2248074
Publication date: 30 June 2014
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-012-0168-y
infinite-state systemsmu-calculusverification of probabilistic systemsverification of well-structured systems
Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items
Forward analysis and model checking for trace bounded WSTS ⋮ Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes ⋮ Handling infinitely branching well-structured transition systems ⋮ On the state complexity of closures and interiors of regular languages with subwords and superwords ⋮ The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings ⋮ Preface to the special issue on probabilistic model checking ⋮ Fixed-Point Elimination in the Intuitionistic Propositional Calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Generalized Post embedding problems
Uses Software
Cites Work
- Undecidability of bisimilarity for Petri nets and some related problems
- Undecidable verification problems for programs with unreliable channels
- Representing hyper-arithmetical sets by equations over sets of integers
- The complexity of finding SUBSEQ\((A)\)
- A note on the attractor-property of infinite-state Markov chains
- Effective constructions in well-partially-ordered free monoids
- Undecidable problems in unreliable computations.
- A well-structured framework for analysing Petri net extensions
- Simulating perfect channels with probabilistic lossy channels
- Algorithmic analysis of programs with well quasi-ordered domains.
- Automata, logics, and infinite games. A guide to current research
- Using forward reachability analysis for verification of lossy channel systems
- On iterating linear transformations over recognizable sets of integers
- Unreliable channels are easier to verify than perfect channels
- Verifying programs with unreliable channels
- On termination and invariance for faulty channel machines
- Petri nets and regular processes
- Quantitative analysis of probabilistic lossy channel systems
- A general approach to comparing infinite-state systems with their finite-state specifications
- The theory of well-quasi-ordering: a frequently discovered concept
- Verification of probabilistic systems with faulty communication
- Verification of Gap-Order Constraint Abstractions of Counter Systems
- LTL with the freeze quantifier and register automata
- The Ordinal-Recursive Complexity of Timed-arc Petri Nets, Data Nets, and Other Enriched Nets
- Multiply-Recursive Upper Bounds with Higman’s Lemma
- Future-Looking Logics on Data Words and Trees
- Alternating-time temporal logic
- Mixing Lossy and Perfect Fifo Channels
- Lossy Counter Machines Decidability Cheat Sheet
- Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
- TaPAS: The Talence Presburger Arithmetic Suite
- Deciding properties of integral relational automata
- A classification of symbolic transition systems
- Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
- Computer Science Logic
- Verification: Theory and Practice
- Tools and Algorithms for the Construction and Analysis of Systems
- CONCUR 2004 - Concurrency Theory
- Computer Aided Verification
- Validation of Stochastic Systems
- On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
- Stochastic Games with Lossy Channels
- Robust Analysis of Timed Automata Via Channel Machines
- Automated Technology for Verification and Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- More on the Size of Higman-Haines Sets: Effective Constructions
- Rudiments of \(\mu\)-calculus
- Well-structured transition systems everywhere!
- Symbolic model checking with rich assertional languages
- Deciding bisimulation-like equivalences with finite-state processes
- Automatic presentations of structures
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Computable fixpoints in well-structured symbolic model checking
