Symbolic Model Checking in Non-Boolean Domains

DOI10.1007/978-3-319-10575-8_31zbMath1392.68259OpenAlexW801429566MaRDI QIDQ3176389

Rupak Majumdar, Jean-François Raskin

Publication date: 20 July 2018

Published in: Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_31

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Combining Model Checking and Deduction

Uses Software

• PHAVer
• HyTech
• Uppaal
• PPL
• UPPAAL TIGA
• Antichains
• FAST
• Acacia+

Cites Work

• 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
• A survey of stochastic \(\omega \)-regular games
• Finding and fixing faults
• Synthesis of Reactive(1) designs
• Antichains and compositional algorithms for LTL synthesis
• Results on the propositional \(\mu\)-calculus
• The octagon abstract domain
• Symbolic model checking: \(10^{20}\) states and beyond
• Borel determinacy
• What's decidable about hybrid automata?
• The modal mu-calculus alternation hierarchy is strict
• A theory of timed automata
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Topology and descriptive set theory
• Reasoning about infinite computations
• Uppaal in a nutshell
• From pre-historic to post-modern symbolic model checking
• Quantitative solution of omega-regular games
• Concurrent reachability games
• Model checking discounted temporal properties
• Approximating the Value of a Concurrent Reachability Game in the Polynomial Time Hierarchy
• Quantitative languages
• Qualitative concurrent parity games
• New results on quantifier elimination over real closed fields and applications to constraint databases
• Value Iteration
• Game Refinement Relations and Metrics
• Antichain Algorithms for Finite Automata
• The complexity of quantitative concurrent parity games
• Grammar Analysis and Parsing by Abstract Interpretation
• Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
• Antichains for the Automata-Based Approach to Model-Checking
• Better Quality in Synthesis through Quantitative Objectives
• An Antichain Algorithm for LTL Realizability
• Graph-Based Algorithms for Boolean Function Manipulation
• Abstract interpretation and application to logic programs
• The determinacy of Blackwell games
• On the synthesis of strategies in infinite games
• On the synthesis of discrete controllers for timed systems
• From program verification to program synthesis
• Programming with angelic nondeterminism
• A classification of symbolic transition systems
• STACS 2004
• Model Checking Quantitative Linear Time Logic
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• CONCUR 2005 – Concurrency Theory
• CONCUR 2003 - Concurrency Theory
• CONCUR 2003 - Concurrency Theory
• Well-structured transition systems everywhere!

This page was built for publication: Symbolic Model Checking in Non-Boolean Domains