Pages that link to "Item:Q3719811"
From MaRDI portal
The following pages link to Automatic verification of finite-state concurrent systems using temporal logic specifications (Q3719811):
Displaying 50 items.
- On temporal logic versus Datalog (Q1401358) (← links)
- Proving properties of continuous systems: Qualitative simulation and temporal logic (Q1402734) (← links)
- Automatic verification of concurrent systems using a formula-based compositional approach (Q1403320) (← links)
- Simplification of boolean verification conditions (Q1575276) (← links)
- Verification of reactive systems using temporal logic with clocks (Q1575841) (← links)
- Stochastic dynamic programming with factored representations (Q1583230) (← links)
- Quantified computation tree logic (Q1603537) (← links)
- A unified language processing methodology (Q1603702) (← links)
- A compiler for MSVL and its applications (Q1630985) (← links)
- Supervisory control and reactive synthesis: a comparative introduction (Q1693819) (← links)
- Generalizing input-driven languages: theoretical and practical benefits (Q1706605) (← links)
- Model checking properties on reduced trace systems (Q1736621) (← links)
- Sublogics of a branching time logic of robustness (Q1740655) (← links)
- Model checking temporal properties of reaction systems (Q1749193) (← links)
- Applying model-checking to solve queries on semistructured data (Q1749228) (← links)
- Cycle detection in computation tree logic (Q1784962) (← links)
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus (Q1801498) (← links)
- Using partial orders for the efficient verification of deadlock freedom and safety properties (Q1801499) (← links)
- An algebraic and algorithmic method for analysing transition systems (Q1822237) (← links)
- Min-max event-triggered computation tree logic (Q1847543) (← links)
- Model checking of systems with many identical timed processes (Q1853589) (← links)
- Specification languages in algebraic compilers (Q1853753) (← links)
- A partial order approach to branching time logic model checking. (Q1854268) (← links)
- Decidable integration graphs. (Q1854273) (← links)
- Module checking (Q1854407) (← links)
- An infinite hierarchy of temporal logics over branching time (Q1854487) (← links)
- Fair simulation (Q1854506) (← links)
- On the complexity of verifying concurrent transition systems (Q1854510) (← links)
- Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking (Q1858428) (← links)
- Is your model checker on time? On the complexity of model checking for timed modal logics (Q1858436) (← links)
- Syntax-directed model checking of sequential programs (Q1858441) (← links)
- On the limits of refinement-testing for model-checking CSP (Q1941896) (← links)
- Verification of a technical system model with linear temporal logic (Q1941912) (← links)
- Formal verification based on Boolean expression diagrams (Q1954165) (← links)
- On logics with two variables (Q1960419) (← links)
- Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\) (Q1989347) (← links)
- Producing explanations for rich logics (Q2024339) (← links)
- IPL: an integration property language for multi-model cyber-physical systems (Q2024345) (← links)
- Branching time logics with multiagent temporal accessibility relations (Q2030777) (← links)
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models (Q2095426) (← links)
- Skeleton abstraction for universal temporal properties (Q2117168) (← links)
- Model checking QCTL plus on quantum Markov chains (Q2123051) (← links)
- Compositional verification of concurrent systems by combining bisimulations (Q2147689) (← links)
- Temporal reasoning through automatic translation of tock-CSP into timed automata (Q2154047) (← links)
- Multiagent temporal logics, unification problems, and admissibilities (Q2160194) (← links)
- Computing race variants in message-passing concurrent programming with selective receives (Q2165226) (← links)
- Cartesian difference categories (Q2200813) (← links)
- Toward model selection by formal methods (Q2229136) (← links)
- Scalable and precise refinement of cache timing analysis via path-sensitive verification (Q2251379) (← links)
- Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes (Q2257984) (← links)
