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
- A complete proof system for propositional projection temporal logic
- Compositional Control Synthesis for Partially Observable Systems
- A technique of state space search based on unfolding
- Automated analysis of mutual exclusion algorithms using CCS
- Proof systems for satisfiability in Hennessy-Milner logic with recursion
- A multiprocess network logic with temporal and spatial modalities
- Title not available (Why is that?)
- Mitigating covert channels based on analysis of the potential for communication
- Model checking concurrent programs
- The Birth of Model Checking
- Augmenting ATL with strategy contexts
- Weighted versus Probabilistic Logics
- On the universal and existential fragments of the \(\mu\)-calculus
- Formal modelling, analysis and verification of hybrid systems
- Relating fair testing and accordance for service replaceability
- On the Complexity of Branching-Time Logics
- Bounded situation calculus action theories
- Characterizing finite Kripke structures in propositional temporal logic
- Analysis of dynamic policies
- A CTL* Model Checker for Petri Nets
- Symbolic computation in automated program reasoning
- Module checking
- Verification of scope-dependent hierarchical state machines
- Automated synthesis of asynchronizations
- Results on the propositional \(\mu\)-calculus
- Weak, strong, and strong cyclic planning via symbolic model checking
- A hierarchy of temporal logics with past
- Verification of multi-linked heaps
- CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
- The Complexity of CTL* + Linear Past
- Model checking and abstraction to the aid of parameterized systems (a survey)
- A transformation-based synthesis of temporal specification
- Is your model checker on time? On the complexity of model checking for timed modal logics
- Refinement modal logic
- A space-efficient on-the-fly algorithm for real-time model checking
- Combining symmetry reduction and under-approximation for symbolic model checking
- Complexity results on branching-time pushdown model checking
- Monitoring metric first-order temporal properties
- Synthesis of Reactive(1) designs
- Solving parity games using an automata-based algorithm
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- Interleaving set temporal logic
- An accessible verification environment for UML models of services
- Question-guided stubborn set methods for state properties
- Undecidable problems in unreliable computations.
- Mathematical modal logic: A view of its evolution
- From Monadic Logic to PSL
- Linear temporal logic symbolic model checking
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)
