“Sometimes” and “not never” revisited
From MaRDI portal
Publication:3766825
DOI10.1145/4904.4999zbMath0629.68020OpenAlexW2004306067MaRDI QIDQ3766825
Joseph Y. Halpern, E. Allen Emerson
Publication date: 1986
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/4904.4999
Logic in computer science (03B70) General topics in the theory of software (68N01) Theory of operating systems (68N25)
Related Items (only showing first 100 items - show all)
Verification of Gap-Order Constraint Abstractions of Counter Systems ⋮ Verification and comparison of transition systems ⋮ Church's Problem Revisited ⋮ Specification and Verification of Multi-Agent Systems ⋮ Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic ⋮ Model-checking CTL* over flat Presburger counter systems ⋮ Introduction to Model Checking ⋮ Temporal Logic and Fair Discrete Systems ⋮ The Complexity of Linear-Time Temporal Logic Model Repair ⋮ A Dynamic Logic with Traces and Coinduction ⋮ Quantified Differential Temporal Dynamic Logic for Verifying Properties of Distributed Hybrid Systems ⋮ Branching Time? Pruning Time! ⋮ Equivalence between model-checking flat counter systems and Presburger arithmetic ⋮ On the Hybrid Extension of CTL and CTL + ⋮ Interleaving set temporal logic ⋮ TTL : a formalism to describe local and global properties of distributed systems ⋮ Generic Infinite Traces and Path-Based Coalgebraic Temporal Logics ⋮ Unnamed Item ⋮ Branching-time logics and fairness, revisited ⋮ Unified temporal logic ⋮ Simulating and model checking membrane systems using strategies in Maude ⋮ Metalevel transformation of strategies ⋮ Unnamed Item ⋮ A tableau construction for finite linear-time temporal logic ⋮ Reasoning About Strategies ⋮ Suitability of the propositional temporal logic to express properties of real-time systems ⋮ Expressiveness and succinctness of a logic of robustness ⋮ A CTL* Model Checker for Petri Nets ⋮ Taming strategy logic: non-recurrent fragments ⋮ \textsc{Pspace}-completeness of the temporal logic of sub-intervals and suffixes ⋮ A survey on compositional algorithms for verification and synthesis in supervisory control ⋮ Cooperative concurrent games ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ Interval Temporal Logic for Visibly Pushdown Systems ⋮ Reasoning About Substructures and Games ⋮ COUNTING TO INFINITY: GRADED MODAL LOGIC WITH AN INFINITY DIAMOND ⋮ HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems ⋮ Solving infinite-domain CSPs using the patchwork property ⋮ Branching vs. Linear Time: Semantical Perspective ⋮ The Birth of Model Checking ⋮ Correcting a Space-Efficient Simulation Algorithm ⋮ A new combination procedure for the word problem that generalizes fusion decidability results in modal logics ⋮ Unnamed Item ⋮ Verification of gap-order constraint abstractions of counter systems ⋮ Proving correctness of labeled transition systems by semantic tableaux ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Interval vs. Point Temporal Logic Model Checking ⋮ Unnamed Item ⋮ Logics of Repeating Values on Data Trees and Branching Counter Systems ⋮ Unnamed Item ⋮ A note on knowledge-based programs and specifications ⋮ On Reasoning About Rings ⋮ A tableau calculus for first-order branching time logic ⋮ Practical reasoning with procedural knowledge ⋮ Reasoning about programs by exploiting the environment ⋮ Equivalences for fair Kripke structures ⋮ Calculational design of a regular model checker by abstract interpretation ⋮ Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic ⋮ Temporal Logic with Recursion. ⋮ COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS ⋮ One-pass Context-based Tableaux Systems for CTL and ECTL ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ Model checking abilities of agents: a closer look ⋮ Incompleteness of states w.r.t. traces in model checking ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Terminating Tableaux for Hybrid Logic with Eventualities ⋮ A Decision Procedure for CTL* Based on Tableaux and Automata ⋮ A clausal resolution method for extended computation tree logic ECTL ⋮ Meanings of Model Checking ⋮ \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\) ⋮ Quantification over sets of possible worlds in branching-time semantics ⋮ Finite-word hyperlanguages ⋮ From Philosophical to Industrial Logics ⋮ Characterizing EF and EX tree logics ⋮ A clausal resolution method for CTL branching-time temporal logic ⋮ Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski ⋮ From Monadic Logic to PSL ⋮ The Complexity of CTL* + Linear Past ⋮ Automatically verifying temporal properties of pointer programs with cyclic proof ⋮ Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach ⋮ Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments ⋮ Analysing Spatial Properties on Neighbourhood Spaces ⋮ Easy Yet Hard: Model Checking Strategies of Agents ⋮ dCTL: A Branching Time Temporal Logic for Fault-Tolerant System Verification ⋮ Egalitarian State-Transition Systems ⋮ On the Complexity of Branching-Time Logics ⋮ Computable CTL * for Discrete-Time and Continuous-Space Dynamic Systems ⋮ An axiomatization of PCTL* ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ On obligations and normative ability: Towards a logical analysis of the social contract ⋮ Logic and Learning ⋮ Verification of Linear Duration Invariants by Model Checking CTL Properties ⋮ Relating word and tree automata ⋮ Automated formal analysis and verification: an overview ⋮ CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
This page was built for publication: “Sometimes” and “not never” revisited
