scientific article

Publication date: 1 November 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

concurrent systems model checking temporal logic automatic verification protocols sequential circuit designs

Hardware implementations of nonnumerical algorithms (VLSI algorithms, etc.) (68W35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Reliability, testing and fault tolerance of networks and computer systems (68M15)

Related Items (only showing first 100 items - show all)

Sequential testing of complex systems: a review ⋮ Unfolding Grammars in Adhesive Categories ⋮ On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking ⋮ Model checking \(\omega \)-regular properties with decoupled search ⋮ Model checking workflow net based on Petri net ⋮ An efficient algorithm for computing bisimulation equivalence ⋮ Quantified epistemic logics for reasoning about knowledge in multi-agent systems ⋮ Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams ⋮ Weighted automata and weighted logics ⋮ Weighted automata and weighted logics with discounting ⋮ Introduction to Model Checking ⋮ Binary Decision Diagrams ⋮ Transfer of Model Checking to Industrial Practice ⋮ Functional Specification of Hardware via Temporal Logic ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Algebraic simulations ⋮ Weighted automata and weighted logics on infinite words ⋮ Symmetry and partial order reduction techniques in model checking Rebeca ⋮ Action language verifier: An infinite-state model checker for reactive software specifications ⋮ Modeling, analyzing and slicing periodic distributed computations ⋮ A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic ⋮ Feature interaction detection by pairwise analysis of LTL properties -- A case study ⋮ Symbolic perimeter abstraction heuristics for cost-optimal planning ⋮ Model checking learning agent systems using Promela with embedded C code and abstraction ⋮ \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes ⋮ Symbolic model checking for channel-based component connectors ⋮ Abstraction for model checking multi-agent systems ⋮ Formally verified algorithms for upper-bounding state space diameters ⋮ Leveraging Horn clause solving for compositional verification of PLC software ⋮ A formal logic approach to constrained combinatorial testing ⋮ Flash memory efficient LTL model checking ⋮ Linear-Time Model Checking: Automata Theory in Practice ⋮ Weighted Automata and Weighted Logics with Discounting ⋮ A canonical form based decision procedure and model checking approach for propositional projection temporal logic ⋮ Symbolic synthesis of masking fault-tolerant distributed programs ⋮ On the use of MTBDDs for performability analysis and verification of stochastic systems. ⋮ Cyclic-routing of unmanned aerial vehicles ⋮ Unfolding Graph Transformation Systems: Theory and Applications to Verification ⋮ Model checking of pushdown systems for projection temporal logic ⋮ The sweep-line state space exploration method ⋮ Model Checking Contracts – A Case Study ⋮ Symbolic Fault Tree Analysis for Reactive Systems ⋮ Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space ⋮ Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction ⋮ Efficient decision procedure for propositional projection temporal logic ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ The Birth of Model Checking ⋮ A satisfiability procedure for quantified Boolean formulae ⋮ Synchronizing relations on words ⋮ Symbolic execution of Reo circuits using constraint automata ⋮ Kripke modelling and verification of temporal specifications of a multiple UAV system ⋮ Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces ⋮ A framework for multi-robot motion planning from temporal logic specifications ⋮ Formal verification based on Boolean expression diagrams ⋮ Symbolic bounded synthesis ⋮ Data Flow Analysis and Testing of Abstract State Machines ⋮ Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic ⋮ Weak Second‐Order Arithmetic and Finite Automata ⋮ Verification of consensus algorithms using satisfiability solving ⋮ An automatic method for the dynamic construction of abstractions of states of a formal model ⋮ A functional formalization of on chip communications ⋮ Exact quantitative probabilistic model checking through rational search ⋮ Quantifier elimination by dependency sequents ⋮ Automated assumption generation for compositional verification ⋮ Bounded semantics ⋮ Toward model selection by formal methods ⋮ Directed Model Checking for B: An Evaluation and New Techniques ⋮ Embedding finite automata within regular expressions ⋮ Efficient SAT-based bounded model checking for software verification ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Maximally permissive controlled system synthesis for non-determinism and modal logic ⋮ Model checking temporal properties of reaction systems ⋮ Verification and enforcement of access control policies ⋮ A decision procedure for propositional projection temporal logic with infinite models ⋮ A data-flow approach to test multi-agent ASMs ⋮ \(\omega\)-regular languages are testable with a constant number of queries ⋮ On the constructive orbit problem ⋮ Abstract reduction in directed model checking CCS processes ⋮ McMillan’s Complete Prefix for Contextual Nets ⋮ From Philosophical to Industrial Logics ⋮ Model-based safety assessment of a triple modular generator with xSAP ⋮ Verifying untimed and timed aspects of the experimental batch plant ⋮ Analysing neurobiological models using communicating automata ⋮ Bounded model checking of traffic light control system ⋮ A formal proof of the deadline driven scheduler in PPTL axiomatic system ⋮ Runtime Verification of Component-Based Systems ⋮ Logic for \(\omega\)-pushdown automata ⋮ Don't care words with an application to the automata-based approach for real addition ⋮ Formal Models of Timing Attacks on Web Privacy ⋮ Specifying and verifying reactive systems in a multi-language environment ⋮ Automatic symmetry detection for Promela ⋮ Counterexample-preserving reduction for symbolic model checking ⋮ Using heuristic search for finding deadlocks in concurrent systems ⋮ Lifted model checking for relational MDPs ⋮ Syntax-directed model checking of sequential programs ⋮ Specification and verification of concurrent programs through refinements ⋮ Towards Deriving Test Sequences by Model Checking ⋮ Weak, strong, and strong cyclic planning via symbolic model checking ⋮ The complexity of automated addition of fault-tolerance without explicit legitimate states ⋮ A framework for compositional nonblocking verification of extended finite-state machines

This page was built for publication: