Automatic verification of finite-state concurrent systems using temporal logic specifications
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 3932379
- A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems
- Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings
- The complexity of probabilistic verification
- scientific article; zbMATH DE number 4128366
Cited in
(only showing first 100 items - show all)- Probabilistic mobile ambients
- Assisting the design of a groupware system - Model checking usability aspects of thinkteam
- Partitioned PLTL model-checking for refined transition systems
- Reasoning about temporal properties of rational play
- Verifying time, memory and communication bounds in systems of reasoning agents
- Automatic symmetry detection for Promela
- Hierarchical verification of asynchronous circuits using temporal logic
- On the analysis of cooperation and antagonism in networks of communicating processes
- Recognizing safety and liveness
- A linear algorithm to solve fixed-point equations on transition systems
- Characterizing finite Kripke structures in propositional temporal logic
- Control machines: A new model of parallelism for compositional specifications and their effective compilation
- TABLEAUX: A general theorem prover for modal logics
- Programming in temporal-nonmonotonic reasoning
- Adequacy-preserving transformations of COSY path programs
- Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings
- A model checker for linear time temporal logic
- Symbolic model checking: \(10^{20}\) states and beyond
- Infinite trees and automaton-definable relations over -words
- A verification system for concurrent programs based on the Boyer-Moore prover
- Verifying automata specification of distributed probabilistic real-time systems
- Information system design of manufacturing environments
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- A theory of timed automata
- An experience in proving regular networks of processes by modular model checking
- Model checking for action-based logics
- A logical query language for hypermedia systems
- Assisting requirement formalization by means of natural language translation
- Safety, liveness and fairness in temporal logic
- A logic for reasoning about time and reliability
- Property preserving abstractions for the verification of concurrent systems
- Using integer programming to verify general safety and liveness properties
- Model-checking discrete duration calculus
- Synchronization trees
- A rewriting approach to binary decision diagrams
- Petri nets for the design and operation of manufacturing systems
- Petri nets, traces, and local model checking
- A temporal logic for real-time partial ordering with named transactions
- Automatic generation of invariants and intermediate assertions
- Model-checking large structured Markov chains.
- On temporal logic versus Datalog
- Proving properties of continuous systems: Qualitative simulation and temporal logic
- Automatic verification of concurrent systems using a formula-based compositional approach
- Simplification of boolean verification conditions
- Verification of reactive systems using temporal logic with clocks
- Stochastic dynamic programming with factored representations
- Quantified computation tree logic
- A unified language processing methodology
- A compiler for MSVL and its applications
- Supervisory control and reactive synthesis: a comparative introduction
- Generalizing input-driven languages: theoretical and practical benefits
- Model checking properties on reduced trace systems
- Sublogics of a branching time logic of robustness
- Model checking temporal properties of reaction systems
- Applying model-checking to solve queries on semistructured data
- Cycle detection in computation tree logic
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- An algebraic and algorithmic method for analysing transition systems
- Min-max event-triggered computation tree logic
- Model checking of systems with many identical timed processes
- Specification languages in algebraic compilers
- A partial order approach to branching time logic model checking.
- Decidable integration graphs.
- Module checking
- An infinite hierarchy of temporal logics over branching time
- Fair simulation
- On the complexity of verifying concurrent transition systems
- Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking
- Is your model checker on time? On the complexity of model checking for timed modal logics
- Syntax-directed model checking of sequential programs
- On the limits of refinement-testing for model-checking CSP
- Verification of a technical system model with linear temporal logic
- Formal verification based on Boolean expression diagrams
- On logics with two variables
- Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
- Producing explanations for rich logics
- IPL: an integration property language for multi-model cyber-physical systems
- Branching time logics with multiagent temporal accessibility relations
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- Skeleton abstraction for universal temporal properties
- Model checking QCTL plus on quantum Markov chains
- Compositional verification of concurrent systems by combining bisimulations
- Temporal reasoning through automatic translation of tock-CSP into timed automata
- Multiagent temporal logics, unification problems, and admissibilities
- Computing race variants in message-passing concurrent programming with selective receives
- Cartesian difference categories
- Toward model selection by formal methods
- Scalable and precise refinement of cache timing analysis via path-sensitive verification
- Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
- Verification of concurrent programs: The automata-theoretic framework
- Automatic and hierarchical verification for concurrent systems
- Model checking Petri nets with MSVL
- Model-checking graded computation-tree logic with finite path semantics
- Translating Xd-C programs to MSVL programs
- A novel approach to verifying context free properties of programs
- Two AGM-style characterizations of model repair
- The model checking fingerprints of CTL operators
- Unified mathematical framework for slicing and symmetry reduction over event structures
- Reasoning about memoryless strategies under partial observability and unconditional fairness constraints
This page was built for publication: Automatic verification of finite-state concurrent systems using temporal logic specifications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3719811)
