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)- Model-checking timed temporal logics
- THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆
- Priority systems with many identical processes
- Resources in process algebra
- A complete proof system for propositional projection temporal logic
- State of the Art in Logics for Verification of Resource-Bounded Multi-Agent Systems
- Three-valued abstraction for probabilistic systems
- Syntax-directed model checking of sequential programs
- Multiphase until formulas over Markov reward models: an algebraic approach
- Undecidable cases of model checking probabilistic temporal-epistemic logic (extended abstract)
- Inf-datalog, Modal Logic and Complexities
- Deciding properties of integral relational automata
- A Logic for Reasoning about Rational Agents
- Formal Verification for Components and Connectors
- Compositional checking of satisfaction
- ATL* Satisfiability Is 2EXPTIME-Complete
- Alternating automata: unifying truth and validity checking for temporal logics
- Automatic verification of distributed systems: the process algebra approach.
- scientific article; zbMATH DE number 2080065 (Why is no real title available?)
- Minimal refinements of specifications in modal and temporal logics
- Minimal refinements of specifications in modal and temporal logics
- A temporal logic for real-time partial ordering with named transactions
- Petri nets, traces, and local model checking
- Sound verification procedures for temporal properties of infinite-state systems
- Translating Xd-C programs to MSVL programs
- On the analysis of cooperation and antagonism in networks of communicating processes
- Meanings of model checking
- scientific article; zbMATH DE number 1497792 (Why is no real title available?)
- Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
- The Birth of Model Checking
- A temporal logic for real-time partial-ordering with named transactions
- A unified language processing methodology
- Extending fairness expressibility of ECTL\(^+\): a tree-style one-pass tableau approach
- Automated temporal reasoning about reactive systems
- A tableau calculus for first-order branching time logic
- Infinite trees and automaton-definable relations over -words
- On ACTL formulas having linear counterexamples
- Automatic verification of concurrent systems using a formula-based compositional approach
- Journeys in non-classical computation I: A grand challenge for computing research
- Multiagent temporal logics, unification problems, and admissibilities
- A formal model for service-oriented interactions
- On the Decision Problem for Two-Variable First-Order Logic
- Model and program repair via group actions
- A data-flow approach to test multi-agent ASMs
- Model-checking graded computation-tree logic with finite path semantics
- Alternating-time stream logic for multi-agent systems
- On the universal and existential fragments of the \(\mu\)-calculus
- State/Event Software Verification for Branching-Time Specifications
- Compositional verification of concurrent systems by combining bisimulations
- Abstract State Machines 2004. Advances in Theory and Practice
- Undecidable verification problems for programs with unreliable channels
- IDD-based model validation of biochemical networks
- An infinite hierarchy of temporal logics over branching time
- Model checking for performability
- CONFLICTS AND FAIR TESTING
- A survey on temporal logics for specifying and verifying real-time systems
- Secure information flow by self-composition
- Model Checking Value-Passing Modal Specifications
- Reasoning about memoryless strategies under partial observability and unconditional fairness constraints
- Sublogics of a branching time logic of robustness
- scientific article; zbMATH DE number 2086795 (Why is no real title available?)
- Model checking for action-based logics
- Improved model checking of hierarchical systems
- Quantified computation tree logic
- Reasoning about networks with many identical finite state processes
- Skeleton abstraction for universal temporal properties
- Specifying and verifying reactive systems in a multi-language environment
- Toward model selection by formal methods
- Linear reachability problems and minimal solutions to linear Diophantine equation systems
- Unified mathematical framework for slicing and symmetry reduction over event structures
- Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic
- Partial-order reduction in the weak modal mu-calculus
- Using integer programming to verify general safety and liveness properties
- Model-checking large structured Markov chains.
- Conformant planning via symbolic model checking and heuristic search
- Verification of \(\mathrm{EB}^3\) specifications using CADP
- Error diagnosis in finite communicating systems
- Strong planning under partial observability
- Symbolic model checking for probabilistic processes
- scientific article; zbMATH DE number 177262 (Why is no real title available?)
- scientific article; zbMATH DE number 4056983 (Why is no real title available?)
- SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
- Characterizing finite Kripke structures in propositional temporal logic
- scientific article; zbMATH DE number 177259 (Why is no real title available?)
- Axioms for real-time logics
- Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
- Dynamic input/output automata: a formal and compositional model for dynamic systems
- Well (and better) quasi-ordered transition systems
- An algebraic and algorithmic method for analysing transition systems
- Cancer hybrid automata: model, beliefs and therapy
- scientific article; zbMATH DE number 177500 (Why is no real title available?)
- Analysis of dynamic policies
- Verifying time, memory and communication bounds in systems of reasoning agents
- Abstract reduction in directed model checking CCS processes
- Characteristic formulae for fixed-point semantics: a general framework
- Quantitative analysis under fairness constraints
- Applying model-checking to solve queries on semistructured data
- A theory of timed automata
- Verifying automata specification of distributed probabilistic real-time systems
- Automated Technology for Verification and Analysis
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)
