Temporal Specifications with Accumulative Values
From MaRDI portal
Publication:2946736
DOI10.1145/2629686zbMath1354.68169OpenAlexW2160029445MaRDI QIDQ2946736
Orna Kupferman, Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2629686
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)
Related Items (23)
Hyperplane separation technique for multidimensional mean-payoff games ⋮ Introduction to Model Checking ⋮ Unnamed Item ⋮ Stochastization of Weighted Automata ⋮ Ratio and Weight Quantiles ⋮ Temporal Specifications with Accumulative Values ⋮ Synthesis for Multi-weighted Games with Branching-Time Winning Conditions ⋮ Quantitative safety and liveness ⋮ Model checking and synthesis for branching multi-weighted logics ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ On the complexity of rational verification ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Quantitative vs. weighted automata ⋮ Quantitative Automata under Probabilistic Semantics ⋮ ``Most of leads to undecidability: failure of adding frequencies to LTL ⋮ Maximizing the Conditional Expected Reward for Reaching the Goal ⋮ Solving Mean-Payoff Games via Quasi Dominions ⋮ Quantitative fair simulation games ⋮ Probabilistic Model Checking for Energy-Utility Analysis ⋮ Nearly Optimal Verifiable Data Streaming ⋮ What's decidable about weighted automata? ⋮ Bidirectional nested weighted automata
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The temporal logic of branching time
- Handbook of weighted automata
- Using branching time temporal logic to synthesize synchronization skeletons
- Reasoning in a restricted temporal logic
- A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
- The complexity of mean payoff games on graphs
- Energy parity games
- Weighted automata and weighted logics
- Semigroups, Presburger formulas, and languages
- Model checking discounted temporal properties
- Branching-Time Model Checking of Parametric One-Counter Automata
- Generalized Mean-payoff and Energy Games
- Temporal Specifications with Accumulative Values
- Church Synthesis Problem for Noisy Input
- The Complexity of Mean-Payoff Automaton Expression
- Quantitative Languages
- When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
- Describing Average- and Longtime-Behavior by Weighted MSO Logics
- On Omega-Languages Defined by Mean-Payoff Conditions
- Better Quality in Synthesis through Quantitative Objectives
- Decidable problems for powerful programs
- Simple Programs Realize Exactly Presburger Formulas
- A really temporal logic
- Finite Automata Computing Real Functions
- Mathematical Foundations of Computer Science 2004
- Mathematical Foundations of Computer Science 2004
- Presburger arithmetic with bounded quantifier alternation
- Lattice Automata
- Automata, Languages and Programming
- On Context-Free Languages
- CONCUR 2003 - Concurrency Theory
This page was built for publication: Temporal Specifications with Accumulative Values
