Modalities for model checking: Branching time logic strikes back
From MaRDI portal
Publication:1820578
DOI10.1016/0167-6423(87)90036-0zbMath0615.68019OpenAlexW1975657455MaRDI QIDQ1820578
Chin-Laung Lei, E. Allen Emerson
Publication date: 1987
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0167-6423(87)90036-0
model checkingspecificationpropositional temporal logicbranching time logicautomatic verification of finite state concurrent programsfinite automata on infinite stringsgeneralized fairness constraintslinear time logic
Formal languages and automata (68Q45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items (56)
Efficient timed model checking for discrete-time systems ⋮ Specification and Verification of Multi-Agent Systems ⋮ Employing symmetry reductions in model checking ⋮ Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic ⋮ Model checking LTL with regular valuations for pushdown systems ⋮ Safety, liveness and fairness in temporal logic ⋮ Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning ⋮ Automata Theory and Model Checking ⋮ Equivalence between model-checking flat counter systems and Presburger arithmetic ⋮ Determinization and limit-determinization of Emerson-Lei automata ⋮ Diagnosability of fair transition systems ⋮ TTL : a formalism to describe local and global properties of distributed systems ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ Unnamed Item ⋮ Problems concerning fairness and temporal logic for conflict-free Petri nets ⋮ A methodology for designing proof rules for fair parallel programs ⋮ To be fair, use bundles ⋮ Mean-payoff games with \(\omega\)-regular specifications ⋮ Off-the-shelf automated analysis of liveness properties for just paths ⋮ Model checking with fairness assumptions using PAT ⋮ Zielonka DAG acceptance and regular languages over infinite words ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ On temporal logic versus Datalog ⋮ Dissecting \texttt{ltlsynt} ⋮ Discriminative Model Checking ⋮ LTL to self-loop alternating automata with generic acceptance and back ⋮ Automated analysis of mutual exclusion algorithms using CCS ⋮ Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic ⋮ Unnamed Item ⋮ A tableau calculus for first-order branching time logic ⋮ Generic Emptiness Check for Fun and Profit ⋮ Certifying inexpressibility ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ A compositional approach to CTL\(^*\) verification ⋮ On model checking for the \(\mu\)-calculus and its fragments ⋮ Meanings of Model Checking ⋮ \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\) ⋮ A clausal resolution method for CTL branching-time temporal logic ⋮ An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps ⋮ Model checking with strong fairness ⋮ Constrained existence problem for weak subgame perfect equilibria with \(\omega \)-regular Boolean objectives ⋮ Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski ⋮ A Rice-style theorem for parallel automata ⋮ Model checking for hybrid branching-time logics ⋮ Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths ⋮ Unnamed Item ⋮ AN NP-COMPLETE FRAGMENT OF LTL ⋮ Temporal logic with recursion ⋮ On global induction mechanisms in aμ-calculus with explicit approximations ⋮ Quantitative Analysis under Fairness Constraints ⋮ On-the-fly Emptiness Check of Transition-Based Streett Automata ⋮ Systolic tree \(\omega\)-languages: The operational and the logical view ⋮ An infinite hierarchy of temporal logics over branching time ⋮ The complexity of propositional linear temporal logics in simple cases ⋮ Global and local views of state fairness ⋮ A taxonomy of fairness and temporal logic problems for Petri nets
This page was built for publication: Modalities for model checking: Branching time logic strikes back
