“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)
CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ Model checking for action-based logics ⋮ Complexity analysis of a unifying algorithm for model checking interval temporal logic ⋮ Assisting requirement formalization by means of natural language translation ⋮ Future temporal logic needs infinitely many modalities ⋮ On the expressive power of temporal logic ⋮ Axiomatization of a branching time logic with indistinguishability relations ⋮ A branching time logic with past operators ⋮ On the universal and existential fragments of the \(\mu\)-calculus ⋮ Complexity results on branching-time pushdown model checking ⋮ Property preserving abstractions for the verification of concurrent systems ⋮ Complexity of finite-variable fragments of propositional temporal and modal logics of computation ⋮ Feature interaction detection by pairwise analysis of LTL properties -- A case study ⋮ Uniform inevitability is tree automaton ineffable ⋮ Reasoning about equilibria in game-like concurrent systems ⋮ A clausal resolution method for branching-time logic \(\text{ECTL}^+\) ⋮ Linear templates of ACTL formulas with an application to SAT-based verification ⋮ HyperPCTL model checking by probabilistic decomposition ⋮ On the freeze quantifier in Constraint LTL: Decidability and complexity ⋮ The complexity of reasoning about knowledge and time. I: Lower bounds ⋮ To be fair, use bundles ⋮ Branching-time logics with path relativisation ⋮ Model checking interval temporal logics with regular expressions ⋮ A propositional probabilistic logic with discrete linear time for reasoning about evidence ⋮ The situation calculus: a case for modal logic ⋮ Preface to the special issue: Temporal logics of agency ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Simulation relations for fault-tolerance ⋮ Counting on CTL\(^*\): On the expressive power of monadic path logic ⋮ Towards categorical models for fairness: Fully abstract presheaf semantics of SCCS with finite delay ⋮ Completeness of a branching-time logic with possible choices ⋮ On temporal logic versus Datalog ⋮ Supervisory control and reactive synthesis: a comparative introduction ⋮ A tableau-based decision procedure for CTL\(^*\) ⋮ Reasoning about graded strategy quantifiers ⋮ Reliability-aware automatic composition approach for web services ⋮ \textit{Once} and \textit{for all} ⋮ Maximal traces and path-based coalgebraic temporal logics ⋮ Branching versus linear logics yet again ⋮ Mathematical modal logic: A view of its evolution ⋮ Reasoning about networks with many identical finite state processes ⋮ Linear temporal logic symbolic model checking ⋮ Model-checking precision agriculture logistics: the case of the differential harvest ⋮ Where logic and agents meet ⋮ Which fragments of the interval temporal logic HS are tractable in model checking? ⋮ Bounded semantics ⋮ Compositionality and bisimulation: A negative result ⋮ Deductive verification of alternating systems ⋮ Finite-word hyperlanguages ⋮ Proving the existence of fair paths in infinite-state systems ⋮ A hierarchy of temporal logics with past ⋮ Sublogics of a branching time logic of robustness ⋮ About the expressive power of CTL combinators ⋮ Arity hierarchy for temporal logics ⋮ GR(1)*: GR(1) specifications extended with existential guarantees ⋮ Strategies, model checking and branching-time properties in Maude ⋮ Formal timing analysis of distributed systems ⋮ Alternating-time temporal logics with linear past ⋮ On the expressive power of hybrid branching-time logics ⋮ Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\) ⋮ Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics ⋮ Inconsistency-tolerant temporal reasoning with hierarchical information ⋮ \(R\)-generability, and definability in branching time logics ⋮ Verification of distributed programs using representative interleaving sequences ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Mitigating covert channels based on analysis of the potential for communication ⋮ Pushdown module checking ⋮ A hierarchy of failures-based models: theory and application ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ Finite identification from the viewpoint of epistemic update ⋮ A compositional approach to CTL\(^*\) verification ⋮ Weak Muller acceptance conditions for tree automata ⋮ On the expressiveness of TPTL and MTL ⋮ On timed alternating simulation for concurrent timed games ⋮ Timed vacuity ⋮ Automatic and hierarchical verification for concurrent systems ⋮ Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy ⋮ Cycle detection in computation tree logic ⋮ Model-checking graded computation-tree logic with finite path semantics ⋮ Model checking for hybrid branching-time logics ⋮ Temporal logic with recursion ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ The model checking fingerprints of CTL operators ⋮ Verification of reactive systems using temporal logic with clocks ⋮ Differential dynamic logic for hybrid systems ⋮ A decidable class of problems for control under partial observation ⋮ An automata-theoretic approach to model-checking systems and specifications over infinite data domains ⋮ Branching-time logics repeatedly referring to states ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models ⋮ Module checking ⋮ An infinite hierarchy of temporal logics over branching time ⋮ Syntax-directed model checking of sequential programs ⋮ Iterated Boolean games ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ A goal-directed decision procedure for hybrid PDL ⋮ Proving partial order properties ⋮ Point algebras for temporal reasoning: Algorithms and complexity ⋮ A unifying semantics for time and events ⋮ Next-preserving branching bisimulation ⋮ Combining symmetry reduction and under-approximation for symbolic model checking
This page was built for publication: “Sometimes” and “not never” revisited
