scientific article; zbMATH DE number 3870578
From MaRDI portal
Publication:3336675
zbMATH Open0546.68014MaRDI QIDQ3336675FDOQ3336675
Edmund Clarke, E. Allen Emerson
Publication date: 1982
Title of this publication is not available (Why is that?)
Recommendations
temporal logicprogram specificationconcurrent programsfinite modelpropositional branching time logicsynchronisation skeletontableau- based decision procedure
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Theory of operating systems (68N25)
Cited In (only showing first 100 items - show all)
- Title not available (Why is that?)
- Structure-based deadlock checking of asynchronous circuits
- Hierarchical cost-parity games
- GR(1)*: GR(1) specifications extended with existential guarantees
- Dependences in strategy logic
- Symbolic model checking of timed guarded commands using difference decision diagrams
- Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
- ATL* Satisfiability Is 2EXPTIME-Complete
- Backdoors for linear temporal logic
- Model checking of pushdown systems for projection temporal logic
- Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics
- Enriched μ–Calculus Pushdown Module Checking
- Model-checking graded computation-tree logic with finite path semantics
- Context-free timed formalisms: robust automata and linear temporal logics
- Compositional Branching-Time Measurements
- A survey on temporal logics for specifying and verifying real-time systems
- Partial-order reduction in the weak modal mu-calculus
- Language and communication problems in formalization: a natural language approach
- Toward model selection by formal methods
- Algebra-based synthesis of loops and their invariants (invited paper)
- Generative program analysis and beyond: the power of domain-specific languages (invited paper)
- Parameter space abstraction and unfolding semantics of discrete regulatory networks
- Taking Some Burden Off an Explicit CTL Model Checker
- Alternating-time temporal logics with linear past
- Inconsistency-tolerant temporal reasoning with hierarchical information
- The Complexity of Linear-Time Temporal Logic Model Repair
- Process Algebra and Model Checking
- Producing explanations for rich logics
- On the Hybrid Extension of CTL and CTL +
- Greening R. Thomas' framework with environment variables: a divide and conquer approach
- One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
- Reasoning about graded strategy quantifiers
- Strategies, model checking and branching-time properties in Maude
- Model Checking Exact Cost for Attack Scenarios
- Deadlock in packet switching networks
- Weak Muller acceptance conditions for tree automata
- Why there is no general solution to the problem of software verification
- Cycle detection in computation tree logic
- An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation
- Natural strategic ability
- Title not available (Why is that?)
- Efficiently Deciding μ-Calculus with Converse over Finite Trees
- Is my attack tree correct?
- Model-checking iterated games
- From Philosophical to Industrial Logics
- Title not available (Why is that?)
- Determinizing monitors for HML with recursion
- Logical vs. behavioural specifications
- Title not available (Why is that?)
- A planner agent that tries its best in presence of nondeterminism
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- Automatically verifying temporal properties of pointer programs with cyclic proof
- A complete axiomatization of weighted branching bisimulation
- Generalized abstraction-refinement for game-based CTL lifted model checking
- On monitoring linear temporal properties
- Model-Checking Counting Temporal Logics on Flat Structures
- A resolution calculus for the branching-time temporal logic CTL
- Title not available (Why is that?)
- Index set expressions can represent temporal logic formulas
- Synthesizing adaptive test strategies from temporal logic specifications
- Next-preserving branching bisimulation
- \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
- Improving parity games in practice
- HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
- A temporal logic for real-time partial ordering with named transactions
- Not all bugs are created equal, but robust reachability can tell the difference
- Clausal resolution in a logic of rational agency
- Counting on CTL\(^*\): On the expressive power of monadic path logic
- Inferring Synchronization under Limited Observability
- An Algorithm for Probabilistic Alternating Simulation
- An infinite hierarchy of temporal logics over branching time
- Quantified computation tree logic
- Probability logics for reasoning about quantum observations
- Synthesis of communicating process skeletons from temporal-spatial logic specifications
- Test generation from P systems using model checking
- A theory of formal synthesis via inductive learning
- Dependences in Strategy Logic
- \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\)
- Vacuity in practice: temporal antecedent failure
- Distributed Synthesis for Alternating-Time Logics
- Approximation Refinement for Interpolation-Based Model Checking
- Assume-guarantee synthesis for digital contract signing
- Verification Modulo theories
- A parametric analysis of the state-explosion problem in model checking
- Program repair without regret
- A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria
- The guarded fragment with transitive guards
- A complete axiom system for propositional projection temporal logic with cylinder computation model
- Synchronous counting and computational algorithm design
- On model checking multiple hybrid views
- A logical query language for hypermedia systems
- Graph Games and Reactive Synthesis
- From non-preemptive to preemptive scheduling using synchronization synthesis
- A hierarchy of failures-based models: theory and application
- Verification of distributed systems with the axiomatic system of MSVL
- Control machines: A new model of parallelism for compositional specifications and their effective compilation
- Automatic symmetry detection for Promela
- A clausal resolution method for extended computation tree logic ECTL
- Complexity of finite-variable fragments of propositional temporal and modal logics of computation
- Arity hierarchy for temporal logics
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3336675)
