Symbolic model checking: \(10^{20}\) states and beyond

From MaRDI portal

Publication:1193587

Jump to:navigation, search

DOI10.1016/0890-5401(92)90017-AzbMath0753.68066MaRDI QIDQ1193587

Edmund M. Clarke, L. J. Hwang, K. L. McMillan, David L. Dill, Jerry R. Burch

Publication date: 27 September 1992

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

binary decision diagrams mu-calculus computation tree logic observational equivalence symbolic representation propositional linear temporal logic finite-state systems model checking algorithm

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Model checking for action-based logics, Extracting unsatisfiable cores for LTL via temporal resolution, An exercise in the automatic verification of asynchronous designs, Randomized OBDD-based graph algorithms, Formal verification of a Java component using the RESOLVE framework, On the universal and existential fragments of the \(\mu\)-calculus, Bounded model checking of infinite state systems, Verification of SpecC using predicate abstraction, Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams, Synthesizing efficient systems in probabilistic environments, Symbolic model checking for probabilistic timed automata, Efficient data structures for Boolean functions, Command-based importance sampling for statistical model checking, Fast and simple nested fixpoints, Practical verification of multi-agent systems against \textsc{Slk} specifications, GSTE is partitioned model checking, Symbolic perimeter abstraction heuristics for cost-optimal planning, Automata-driven partial order reduction and guided search for LTL model checking, Symbolic techniques in satisfiability solving, State based control of timed discrete event systems using binary decision diagrams, Offline and online monitoring of scattered uncertain logs using uncertain linear dynamical systems, On the number of active states in deterministic and nondeterministic finite automata, Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes, MR4UM: a framework for adding fault tolerance to UML state diagrams, Petri nets, traces, and local model checking, An improved algorithm for the evaluation of fixpoint expressions, Program schemata vs. automata for decidability of program logics, Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving, Symbolic synthesis of masking fault-tolerant distributed programs, Exponential improvement of time complexity of model checking for multiagent systems with perfect recall, On the expressivity and complexity of quantitative branching-time temporal logics, Solving parity games by a reduction to SAT, Well-abstracted transition systems: Application to FIFO automata., Agent planning programs, A satisfiability procedure for quantified Boolean formulae, Bisimulation conversion and verification procedure for goal-based control systems, Towards a notion of unsatisfiable and unrealizable cores for LTL, Exploiting step semantics for efficient bounded model checking of asynchronous systems, Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces, SAT-solving in CSP trace refinement, An explicit transition system construction approach to LTL satisfiability checking, On symbolic OBDD-based algorithms for the minimum spanning tree problem, Formal verification based on Boolean expression diagrams, Symbolic bounded synthesis, Discrete-time control for rectangular hybrid automata, Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search, Plan aggregation for strong cyclic planning in nondeterministic domains, Binary decision diagrams for first-order predicate logic., Linear temporal logic symbolic model checking, Model checking RAISE applicative specifications, First-order temporal logic monitoring with BDDs, Symbolic state-space exploration and numerical analysis of state-sharing composed models, Static analysis and stochastic search for reachability problem, Property-directed incremental invariant generation, Model checking properties on reduced trace systems, Symbolic coloured SCC decomposition, A hierarchy of temporal logics with past, An introduction to mechanized reasoning, Hybrid and subexponential linear logics, The complexity of counting models of linear-time temporal logic, Enhancing unsatisfiable cores for LTL with information on temporal relevance, Symbolic model checking: \(10^{20}\) states and beyond, Component-wise incremental LTL model checking, Synthesis of obfuscation policies to ensure privacy and utility, Specification and automatic verification of self-timed queues, Verification and enforcement of access control policies, Automatic verification of distributed systems: the process algebra approach., Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems, A symbolic model for timed concurrent constraint programming, IDD-based model validation of biochemical networks, Compositional reasoning for shared-variable concurrent programs, Approximate verification of strategic abilities under imperfect information, Representation of graphs by OBDDs, A formal semantics of extended hierarchical state transition matrices using CSP\#, On the number of active states in finite automata, Structuring and automating hardware proofs in a higher-order theorem- proving environment, Generating extended resolution proofs with a BDD-based SAT solver, Two AGM-style characterizations of model repair, A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria, Partitioned PLTL model-checking for refined transition systems, Hybrid systems: From verification to falsification by combining motion planning and discrete search, Symbolic model checking for \(\mu\)-calculus requires exponential time, An automata-theoretic approach to model-checking systems and specifications over infinite data domains, Model checking for hybrid logic, Stochastic dynamic programming with factored representations, Counterexample-preserving reduction for symbolic model checking, Terminal satisfiability in GSTE, Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models, Decidable integration graphs., Specification in CTL + past for verification in CTL., Iterating transducers, Syntax-directed model checking of sequential programs, Lazy regular sensing, A theory of timed automata, Weak, strong, and strong cyclic planning via symbolic model checking, Conformant planning via symbolic model checking and heuristic search, The complexity of automated addition of fault-tolerance without explicit legitimate states, Improving the filtering of branch-and-bound MDD solver, Distributed symbolic model checking for \(\mu\)-calculus, Combining symmetry reduction and under-approximation for symbolic model checking, Partial Order Reduction for Deep Bug Finding in Synchronous Hardware, Model checking workflow net based on Petri net, Binary Decision Diagrams, BDD-Based Symbolic Model Checking, Combining Model Checking and Testing, Symbolic Model Checking in Non-Boolean Domains, Model-checking for real-time systems, Model Checking of Biological Systems, Randomized OBDD-Based Graph Algorithms, Controller/Orchestrator Synthesis via Filtration, Exploiting interleaving semantics in symbolic state-space generation, Program verification with interacting analysis plugins, When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus, The state of SAT, Symbolic Model Checking for Alternating Projection Temporal Logic, Model Checking Linear-Time Properties of Probabilistic Systems, Unnamed Item, Symbolic model checking for probabilistic processes, Ordered Binary Decision Diagrams and the Davis-Putnam procedure, Regular model checking: evolution and perspectives, I/O automata in Isabelle/HOL, Towards better heuristics for solving bounded model checking problems, A survey on compositional algorithms for verification and synthesis in supervisory control, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Linear-Time Model Checking: Automata Theory in Practice, Revising system specifications in temporal logic, Assumption-based runtime verification, Universal algorithms for parity games and nested fixpoints, Symbolic verification and strategy synthesis for turn-based stochastic games, Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic, A decision diagram operation for reachability, A proof system for unified temporal logic, Model Checking Contracts – A Case Study, Hierarchical Set Decision Diagrams and Automatic Saturation, The Birth of Model Checking, Saturation Enhanced with Conditional Locality: Application to Petri Nets, Automated deduction in a graphical temporal logic, Unnamed Item, Temporal property verification as a program analysis task, Unnamed Item, Priority functions for the approximation of the metric TSP, Generating diagnostic information for behavioral preorders, Properties of a predicate transformer of the VRS system, An automatic method for the dynamic construction of abstractions of states of a formal model, Strong planning under partial observability, Directed Model Checking for B: An Evaluation and New Techniques, Statistical Verification of Probabilistic Properties with Unbounded Until, Concurrent reachability games, On the Unusual Effectiveness of Logic in Computer Science, Symbolic topological sorting with OBDDs, Automated Generation of Optimal Controllers through Model Checking Techniques, Symbolic graphs: Linear solutions to connectivity related problems, One-pass Context-based Tableaux Systems for CTL and ECTL, A discrete event systems approach to network fault management: detection and diagnosis of faults, ACTLW -- an action-based computation tree logic with unless operator, Unnamed Item, Symbolic Bisimulation for Quantum Processes, Weakest Invariant Generation for Automated Addition of Fault-Tolerance, Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols, Abstractions of data types, Size of OBDD representation of 2-level redundancies functions, Well-structured transition systems everywhere!, Symbolic model checking with rich assertional languages, A method for the verification of a distributed and synchronized algorithm, Verification by augmented abstraction: The automata-theoretic view, From Philosophical to Industrial Logics, Model checking with strong fairness, The Edge of Graph Transformation — Graphs for Behavioural Specification, Qualitative criteria of admissibility for enforced agreements, Model checking for a class of weighted automata, From Monadic Logic to PSL, A contribution to the validation of grafcet controlled systems, Automata-Theoretic Model Checking Revisited, Well (and Better) Quasi-Ordered Transition Systems, SAT-Based Model Checking without Unrolling, Bounded model checking of traffic light control system, Compositional Model Checking of product-form CTMCs, Unnamed Item, Runtime Verification of Component-Based Systems, BDD-based decision procedures for the modal logic K ★, Hybrid linear logic, revisited, Formal Models of Timing Attacks on Web Privacy, ON REACHABILITY AND SAFETY IN INFINITE-STATE SYSTEMS, Bounded Model Checking for Partial Kripke Structures, Discrete-time control for rectangular hybrid automata, VERIFYING VERY LARGE INDUSTRIAL CIRCUITS USING 100 PROCESSES AND BEYOND, From complementation to certification, An interpolating theorem prover, Automated formal analysis and verification: an overview, Undecidable verification problems for programs with unreliable channels

Cites Work

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:1193587&oldid=13251275"