From liveness to promptness

DOI10.1007/s10703-009-0067-zzbMath1192.68416OpenAlexW3002839602MaRDI QIDQ1039845

Orna Kupferman, Moshe Y. Vardi, Nir Piterman

Publication date: 23 November 2009

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-009-0067-z

zbMATH Keywords

verificationlivenesstemporal logic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in artificial intelligence (68T27) Temporal logic (03B44)

Related Items

Delay Games with WMSO$$+$$U Winning Conditions, Parameterized linear temporal logics meet costs: still not costlier than LTL, Model checking interval temporal logics with regular expressions, Optimal bounds in parametric LTL games, Robust, expressive, and quantitative linear temporal logics: pick any two for free, Delay Games with WMSO+U Winning Conditions, An interface theory for service-oriented design, Realizability problem for constraint LTL, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Hierarchical cost-parity games, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Parametric metric interval temporal logic, Model checking algorithms for hyperproperties (invited paper), Beyond \(\omega \)-regular languages: \(\omega T\)-regular expressions and their automata and logic counterparts, Parametric linear dynamic logic, Cycle detection in computation tree logic, Distributed synthesis for parameterized temporal logics, Quantitative reductions and vertex-ranked infinite games, Natural strategic ability, How Much Lookahead is Needed to Win Infinite Games?, Quantifying Bounds in Strategy Logic, Prompt Interval Temporal Logic, Looking at mean-payoff and total-payoff through windows, Timed games with bounded window parity objectives

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• Defining liveness
• The complementation problem for Büchi automata with applications to temporal logic
• Reasoning about infinite computations
• Parametric temporal logic for “model measuring”
• Automata for the modal μ-calculus and related results
• Solving Sequential Conditions by Finite-State Strategies
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Depth-First Search and Linear Graph Algorithms
• Faster Algorithms for Finitary Games
• Tools and Algorithms for the Construction and Analysis of Systems