scientific article; zbMATH DE number 3870578
From MaRDI portal
Publication:3336675
zbMATH Open0546.68014MaRDI QIDQ3336675FDOQ3336675
Authors: 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)
- Dependences in strategy logic
- \(\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 infinite hierarchy of temporal logics over branching time
- Quantified computation tree logic
- Probability logics for reasoning about quantum observations
- An algorithm for probabilistic alternating simulation
- 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
- \(\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
- Introduction to model checking
- Complexity of finite-variable fragments of propositional temporal and modal logics of computation
- Arity hierarchy for temporal logics
- On feasible cases of checking multi-agent systems behavior.
- On the semantics of strategy logic
- Determinization and memoryless winning strategies
- Code aware resource management
- Title not available (Why is that?)
- Title not available (Why is that?)
- A theoretical foundation of the DSSSL location model
- Global and local views of state fairness
- Bounded model checking of traffic light control system
- Translating Java for multiple model checkers: The Bandera back-end
- Interpretability of first-order linear temporal logics in fork algebras
- Synthesizing synchronous systems by static scheduling in space-time
- 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
- Process algebra and model checking
- ATL* Satisfiability Is 2EXPTIME-Complete
- Backdoors for linear temporal logic
- On the complexity of \(\mathsf{ATL}\) and \(\mathsf{ATL}^*\) module checking
- 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
- 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
- Results on alternating-time temporal logics with linear past
- Alternating-time temporal logics with linear past
- Inconsistency-tolerant temporal reasoning with hierarchical information
- The Complexity of Linear-Time Temporal Logic Model Repair
- Producing explanations for rich logics
- On the Hybrid Extension of CTL and CTL +
- Modal logics for nominal transition systems
- Tutorial on parameterized model checking of fault-tolerant distributed algorithms
- 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
- Compositional branching-time measurements
- 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?)
- Is my attack tree correct?
- Model-checking iterated games
- From Philosophical to Industrial Logics
- Determinizing monitors for HML with recursion
- Efficiently deciding \(\mu\)-calculus with converse over finite trees
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)
