scientific article

Publication date: 1982

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

CSP validation communicating sequential processes algorithmic description fixed points of monotonic predicate transformers interpreted Petri net

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theory of operating systems (68N25)

Related Items

Partial-order reduction in the weak modal mu-calculus, Regular model checking: evolution and perspectives, SMT-based verification of program changes through summary repair, Verification Modulo theories, Revising system specifications in temporal logic, Symbolic analysis of linear hybrid automata -- 25 years later, A pragmatic approach to stateful partial order reduction, A space-efficient on-the-fly algorithm for real-time model checking, Operational causality -- necessarily sufficient and sufficiently necessary, Symbolic model checking with rich assertional languages, Automatic verification of parameterized networks of processes, \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers, Compositional analysis for verification of parameterized systems, Sémantique asynchrone et comportements infinis en CPS, Two normal form theorems for CSP programs, Introduction to Model Checking, Temporal Logic and Fair Discrete Systems, Combining Model Checking and Testing, Combining Model Checking and Deduction, Transfer of Model Checking to Industrial Practice, Algebraic simulations, Multi-Valued Reasoning about Reactive Systems, Structure-based deadlock checking of asynchronous circuits, Coverage metrics for temporal logic model checking, A mechanism of function calls in MSVL, Recent advances in program verification through computer algebra, Unnamed Item, Formal modeling and verification for MVB, Polynomial interrupt timed automata: verification and expressiveness, A theory of formal synthesis via inductive learning, Dependences in Strategy Logic, Unnamed Item, Reasoning About Strategies, A complete proof system for propositional projection temporal logic, rCOS: Defining Meanings of Component-Based Software Architectures, Formal Modelling, Analysis and Verification of Hybrid Systems, Enriched μ–Calculus Pushdown Module Checking, Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving, On the semantics of strategy logic, Linear-Time Model Checking: Automata Theory in Practice, A complete axiom system for propositional projection temporal logic with cylinder computation model, Model checking and synthesis for branching multi-weighted logics, Reasoning About Substructures and Games, Augmenting ATL with strategy contexts, Supervisory control and reactive synthesis: a comparative introduction, A proof system for unified temporal logic, Branching vs. Linear Time: Semantical Perspective, A sound and complete proof system for a unified temporal logic, Complete Abstractions and Subclassical Modal Logics, \textsc{NeVer}: a tool for artificial neural networks verification, The Birth of Model Checking, Towards a notion of unsatisfiable and unrealizable cores for LTL, Reasoning about graded strategy quantifiers, Automated analysis of mutual exclusion algorithms using CCS, Unnamed Item, Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems, Interrupt timed automata: verification and expressiveness, Explaining counterexamples using causality, Reasoning about networks with many identical finite state processes, Model-checking precision agriculture logistics: the case of the differential harvest, Temporal normal form for Linear Temporal Logic formulae1, CTL Model-Checking with Graded Quantifiers, Control machines: A new model of parallelism for compositional specifications and their effective compilation, Calculational design of a regular model checker by abstract interpretation, Dependences in strategy logic, The modeling library of eavesdropping methods in quantum cryptography protocols by model checking, Beyond vacuity: towards the strongest passing formula, An Automata-Theoretic Approach to Infinite-State Systems, Vacuity in practice: temporal antecedent failure, On the order of test goals in specification-based testing, Meanings of Model Checking, Smaller Abstractions for ∀CTL* without Next, On complexity of verification of interacting agents' behavior, Formal language properties of hybrid systems with strong resets, Tutorial on Model Checking: Modelling and Verification in Computer Science, From Philosophical to Industrial Logics, Model checking with strong fairness, An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation, ATL with Strategy Contexts and Bounded Memory, Fifty years of Hoare's logic, Synthesizing adaptive test strategies from temporal logic specifications, From Monadic Logic to PSL, Automata-Theoretic Model Checking Revisited, Natural strategic ability, A novel approach to verifying context free properties of programs, Using partial orders for the efficient verification of deadlock freedom and safety properties, Improving parity games in practice, Unnamed Item, A formal proof of the deadline driven scheduler in PPTL axiomatic system, Automatically verifying temporal properties of pointer programs with cyclic proof, Program repair without regret, Unnamed Item, Logical vs. behavioural specifications, Branching-Time Temporal Logics with Minimal Model Quantifiers, Partitioned PLTL model-checking for refined transition systems, Runtime Verification of Component-Based Systems, Solving Parity Games Using an Automata-Based Algorithm, Alternating automata: Unifying truth and validity checking for temporal logics, Local proofs for global safety properties, Systems of agents controlled by logical programs: complexity of verification, Automatic symmetry detection for Promela, Probabilistic temporal logics via the modal mu-calculus, Measuring and Synthesizing Systems in Probabilistic Environments, Model checking for hybrid logic, Model checking of systems with many identical timed processes, Module checking, Automated formal analysis and verification: an overview, An experience in proving regular networks of processes by modular model checking, Next-preserving branching bisimulation, Verifying time partitioning in the DEOS scheduling kernel, Combining symmetry reduction and under-approximation for symbolic model checking

Uses Software

CESAR