Model checking discounted temporal properties

DOI10.1016/j.tcs.2005.07.033zbMath1079.68062OpenAlexW2109187338MaRDI QIDQ2575738

Luca de Alfaro, Marco Faella, Rupak Majumdar, Thomas A. Henzinger, Mariëlle I. A. Stoelinga

Publication date: 6 December 2005

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.07.033

zbMATH Keywords

Markov chainsMarkov decision processestransition systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (23)

Specification and Verification of Multi-Agent Systems ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Nondeterministic finite automata based on quantum logic: language equivalence relation and robustness ⋮ Temporal Specifications with Accumulative Values ⋮ Quantitative safety and liveness ⋮ Model checking computation tree logic over finite lattices ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ Quantitative model checking of linear-time properties based on generalized possibility measures ⋮ Computing branching distances with quantitative games ⋮ Model checking games for the quantitative \(\mu \)-calculus ⋮ On weighted first-order logics with discounting ⋮ Nondeterministic fuzzy automata with membership values in complete residuated lattices ⋮ Synthesis from component libraries with costs ⋮ Model Checking Quantitative Linear Time Logic ⋮ Model checking fuzzy computation tree logic ⋮ Parametric and Quantitative Extensions of Modal Transition Systems ⋮ On High-Quality Synthesis ⋮ Quantitative analysis of weighted transition systems ⋮ Natural strategic ability ⋮ Compositionality for quantitative specifications ⋮ Computation tree measurement language (CTML) ⋮ Multi-valued Verification of Strategic Ability ⋮ Simulation for lattice-valued doubly labeled transition systems

Cites Work

• The complexity of mean payoff games on graphs
• Bisimulation for labelled Markov processes
• Model checking of probabilistic and nondeterministic systems
• Probability with Martingales
• Tools and Algorithms for the Construction and Analysis of Systems
• CONCUR 2003 - Concurrency Theory
• 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: Model checking discounted temporal properties