Automatic verification of finite-state concurrent systems using temporal logic specifications
From MaRDI portal
Publication:3719811
DOI10.1145/5397.5399zbMath0591.68027OpenAlexW2117189826WikidataQ55918946 ScholiaQ55918946MaRDI QIDQ3719811
A. P. Sistla, E. Allen Emerson, Edmund M. Clarke
Publication date: 1986
Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: http://www.acm.org/pubs/contents/journals/toplas/1986-8/
Related Items
Characteristic formulae for fixed-point semantics: a general framework, Model checking QCTL plus on quantum Markov chains, Model-checking for resource-bounded ATL with production and consumption of resources, Model checking mobile ad hoc networks, Complexity of Model Checking for Modal Dependence Logic, On the universal and existential fragments of the \(\mu\)-calculus, Compositional analysis for verification of parameterized systems, A compiler for MSVL and its applications, Resources in process algebra, Complexity results on branching-time pushdown model checking, Symbolic model checking for probabilistic timed automata, Dynamic input/output automata: a formal and compositional model for dynamic systems, Compositional verification of concurrent systems by combining bisimulations, Using Evolution Graphs for Describing Topology-Aware Prediction Models in Large Clusters, Temporal reasoning through automatic translation of tock-CSP into timed automata, Symbolic model checking for channel-based component connectors, Maintenance goals of agents in a dynamic environment: formulation and policy construction, Assembling a consistent set of sentences in relational probabilistic logic with stochastic independence, Multiagent temporal logics, unification problems, and admissibilities, Computing race variants in message-passing concurrent programming with selective receives, Unified temporal logic, Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization, A survey on temporal logics for specifying and verifying real-time systems, Reasoning About Substructures and Games, Verifying a scheduling protocol of safety-critical systems, Supervisory control and reactive synthesis: a comparative introduction, A proof system for unified temporal logic, On the limits of refinement-testing for model-checking CSP, Verification of a technical system model with linear temporal logic, Cartesian difference categories, Generalizing input-driven languages: theoretical and practical benefits, Formal verification based on Boolean expression diagrams, Temporal property verification as a program analysis task, Deadlock-freedom in component systems with architectural constraints, On logics with two variables, Cancer hybrid automata: model, beliefs and therapy, Toward model selection by formal methods, Strong planning under partial observability, Model checking properties on reduced trace systems, Sublogics of a branching time logic of robustness, On the Unusual Effectiveness of Logic in Computer Science, Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\), Model checking temporal properties of reaction systems, Applying model-checking to solve queries on semistructured data, COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS, FSP and FLTL framework for specification and verification of middle-agents, Planning temporal events using point-interval logic, AN EXPRESSIVE EXTENSION OF TLC, Scalable and precise refinement of cache timing analysis via path-sensitive verification, Probabilistic verification and approximation, Model checking abilities of agents: a closer look, Observations in using parallel and sequential evolutionary algorithms for automatic software testing, Analysis of dynamic policies, Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes, Model checking expected time and expected reward formulae with random time bounds, \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\), Quantification over sets of possible worlds in branching-time semantics, Producing explanations for rich logics, IPL: an integration property language for multi-model cyber-physical systems, Verification of concurrent programs: The automata-theoretic framework, Automatic and hierarchical verification for concurrent systems, Cycle detection in computation tree logic, Model checking Petri nets with MSVL, An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps, Branching time logics with multiagent temporal accessibility relations, Statistical probabilistic model checking with a focus on time-bounded properties, Model-checking graded computation-tree logic with finite path semantics, A contribution to the validation of grafcet controlled systems, Verifying untimed and timed aspects of the experimental batch plant, Well (and Better) Quasi-Ordered Transition Systems, Translating Xd-C programs to MSVL programs, A novel approach to verifying context free properties of programs, 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, Two AGM-style characterizations of model repair, Compositional Model Checking of product-form CTMCs, Group-by-Group Probabilistic Bisimilarities and Their Logical Characterizations, An algebraic and algorithmic method for analysing transition systems, The model checking fingerprints of CTL operators, Specifying and verifying reactive systems in a multi-language environment, Model checking for performability, Probabilistic temporal logics via the modal mu-calculus, Min-max event-triggered computation tree logic, Unified mathematical framework for slicing and symmetry reduction over event structures, Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models, A semantic framework for the abstract model checking of tccp programs, 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, Validating for Liveness in Hidden Adversary 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, Reasoning about memoryless strategies under partial observability and unconditional fairness constraints, Exogenous Probabilistic Computation Tree Logic, Skeleton abstraction for universal temporal properties, Skeleton Abstraction for Universal Temporal Properties, Verification and comparison of transition systems, Specification and Verification of Multi-Agent Systems, State of the Art in Logics for Verification of Resource-Bounded Multi-Agent Systems, Temporal Logic and Fair Discrete Systems, BDD-Based Symbolic Model Checking, Combining Model Checking and Testing, Model Checking Real-Time Systems, Model Checking Value-Passing Modal Specifications, Model Checking of Biological Systems, Multi-Valued Reasoning about Reactive Systems, TTL : a formalism to describe local and global properties of distributed systems, Unnamed Item, Verifying Systems of Resource-Bounded Agents, Symbolic model checking for probabilistic processes, A temporal logic for real-time partial-ordering with named transactions, Expressiveness and succinctness of a logic of robustness, Partial-order reduction in the weak modal mu-calculus, Regular model checking: evolution and perspectives, An (almost) fuzzy logic of action and preferences, its quasi-model interpretations, and the problem of its decidability, Zielonka DAG acceptance and regular languages over infinite words, Dynamic temporal logical operations in multi-agent logics, Taming strategy logic: non-recurrent fragments, A survey on compositional algorithms for verification and synthesis in supervisory control, Linear-Time Model Checking: Automata Theory in Practice, Model and program repair via group actions, Revising system specifications in temporal logic, Branching vs. Linear Time: Semantical Perspective, Mechanizing the Powerset Construction for Restricted Classes of ω-Automata, The Birth of Model Checking, New Challenges in Model Checking, Automated deduction in a graphical temporal logic, ATL* Satisfiability Is 2EXPTIME-Complete, On the Decision Problem for Two-Variable First-Order Logic, Proving correctness of labeled transition systems by semantic tableaux, Unnamed Item, Unnamed Item, Data Flow Analysis and Testing of Abstract State Machines, Unnamed Item, Knowledge-based programs, On Reasoning About Rings, Local model checking for context-free processes, A tableau calculus for first-order branching time logic, Deciding properties of integral relational automata, Equivalences for fair Kripke structures, Compositionality in state space verification methods, Inf-datalog, Modal Logic and Complexities, Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic, Analysing Biochemical Oscillation through Probabilistic Model Checking, Minimal refinements of specifications in modal and temporal logics, One-pass Context-based Tableaux Systems for CTL and ECTL, A resolution calculus for the branching-time temporal logic CTL, INDUCTIVE COMPOSITION OF NUMBERS WITH MAXIMUM, MINIMUM, AND ADDITION: A New Theory for Program Execution-Time Analysis, Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities, Fair simulation, Refining and Compressing Abstract Model Checking1 1The work is partially supported by MURST project: Certificazione automatica di programmi mediante interpretazione astratta., Modeling Concurrent systems specified in a Temporal Concurrent Constraint language-I, Model Theoretic Syntax and Parsing, Minimal refinements of specifications in modal and temporal logics, A menagerie of timed automata, An Automata-Theoretic Approach to Infinite-State Systems, Min-max Computation Tree Logic, Symbolic model checking with rich assertional languages, Automatic verification of parameterized networks of processes, On ACTL formulas having linear counterexamples, Meanings of Model Checking, From Philosophical to Industrial Logics, A Logic for Reasoning about Rational Agents, A clausal resolution method for CTL branching-time temporal logic, Models and logics for true concurrency., Logical models of discrete even systems: a comparative exposition, Unnamed Item, Axioms for real-time logics, Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski, Model checking for a class of weighted automata, From Monadic Logic to PSL, Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints, An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures, Automata-Theoretic Model Checking Revisited, Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach, Formal Verification for Components and Connectors, Easy Yet Hard: Model Checking Strategies of Agents, Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall, dCTL: A Branching Time Temporal Logic for Fault-Tolerant System Verification, The Complexity of Satisfiability for Fragments of CTL and CTL⋆, Model-checking Timed Temporal Logics, THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆, Computable CTL * for Discrete-Time and Continuous-Space Dynamic Systems, CONFLICTS AND FAIR TESTING, BDD-based decision procedures for the modal logic K ★, Constructive knowledge: what agents can achieve under imperfect information, Petri nets, traces, and local model checking, Quantitative Analysis under Fairness Constraints, Secure information flow by self-composition, Alternating automata: Unifying truth and validity checking for temporal logics, Journeys in non-classical computation I: A grand challenge for computing research, Model Checking and Validity in Propositional and Modal Inclusion Logics, Undecidable verification problems for programs with unreliable channels, Property-oriented expansion, Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic, A space-efficient on-the-fly algorithm for real-time model checking, Operational causality -- necessarily sufficient and sufficiently necessary, Construction of deterministic transition graphs from dynamic integrity constraints, Model checking for action-based logics, A logical query language for hypermedia systems, Assisting requirement formalization by means of natural language translation, Verification of \(\mathrm{EB}^3\) specifications using CADP, Completeness and decidability results for CTL in constructive type theory, Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners, Safety, liveness and fairness in temporal logic, A logic for reasoning about time and reliability, Property preserving abstractions for the verification of concurrent systems, Model-checking discrete duration calculus, Synchronization trees, A rewriting approach to binary decision diagrams, On the analysis of cooperation and antagonism in networks of communicating processes, Recognizing safety and liveness, The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems, Synthesis of large dynamic concurrent programs from dynamic specifications, Data structures for symbolic multi-valued model-checking, A linear algorithm to solve fixed-point equations on transition systems, Petri nets for the design and operation of manufacturing systems, Characterizing finite Kripke structures in propositional temporal logic, Modeling dynamic reconfigurations in Reo using high-level replacement systems, A complete proof system for propositional projection temporal logic, Petri nets, traces, and local model checking, A temporal logic for real-time partial ordering with named transactions, A state/event-based model-checking approach for the analysis of abstract system properties, Trace-based verification of imperative programs with I/O, Minimal probabilistic P systems for modelling ecological systems, Multiphase until formulas over Markov reward models: an algebraic approach, Model-checking large structured Markov chains., On temporal logic versus Datalog, Proving properties of continuous systems: Qualitative simulation and temporal logic, Improved model checking of hierarchical systems, \textsc{NeVer}: a tool for artificial neural networks verification, A reduced maximality labeled transition system generation for recursive Petri nets, A quantitative study of pure parallel processes, Kripke modelling and verification of temporal specifications of a multiple UAV system, A formal model for service-oriented interactions, A novel logic-based automatic approach to constructing compliant security policies, \textit{Once} and \textit{for all}, Three-valued abstraction for probabilistic systems, Static analysis of IMC, Feasibility analysis for robustness quantification by symbolic model checking, Reasoning about networks with many identical finite state processes, Linear temporal logic symbolic model checking, Where logic and agents meet, Specification of communicating processes: temporal logic versus refusals-based refinement, 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, A hierarchy of temporal logics with past, About the expressive power of CTL combinators, Compilation of the ELECTRE reactive language into finite transition systems, Arity hierarchy for temporal logics, An introduction to mechanized reasoning, A model checker for linear time temporal logic, Symbolic model checking: \(10^{20}\) states and beyond, On-line compositional controller synthesis for AGV, Synthesis of obfuscation policies to ensure privacy and utility, On the axiomatizability of some first-order spatio-temporal theories, Complexity of validity for propositional dependence logics, The modeling library of eavesdropping methods in quantum cryptography protocols by model checking, A stubborn attack on state explosion, Compositional checking of satisfaction, Infinite trees and automaton-definable relations over \(\omega\)-words, Automatic verification of distributed systems: the process algebra approach., Combining partial-order reductions with on-the-fly model-checking., Computation tree logic model checking based on possibility measures, A data-flow approach to test multi-agent ASMs, Alternating-time stream logic for multi-agent systems, IDD-based model validation of biochemical networks, Linear reachability problems and minimal solutions to linear Diophantine equation systems, Abstract reduction in directed model checking CCS processes, Probabilistic mobile ambients, A formal proof of the deadline driven scheduler in PPTL axiomatic system, Assisting the design of a groupware system - Model checking usability aspects of thinkteam, A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria, Partitioned PLTL model-checking for refined transition systems, Verifying automata specification of distributed probabilistic real-time systems, Priority systems with many identical processes, Reasoning about temporal properties of rational play, Game-theoretic simulation checking tool, Verifying time, memory and communication bounds in systems of reasoning agents, Information system design of manufacturing environments, Simplification of boolean verification conditions, Verification of reactive systems using temporal logic with clocks, Automatic symmetry detection for Promela, Stochastic dynamic programming with factored representations, Quantified computation tree logic, A unified language processing methodology, A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol, Hierarchical verification of asynchronous circuits using temporal logic, A theory of timed automata, Point algebras for temporal reasoning: Algorithms and complexity, Conformant planning via symbolic model checking and heuristic search, An experience in proving regular networks of processes by modular model checking, Verifying time partitioning in the DEOS scheduling kernel, Distributed symbolic model checking for \(\mu\)-calculus, Reduced models for efficient CCS verification, Combining symmetry reduction and under-approximation for symbolic model checking
Uses Software
