scientific article

Publication date: 1982

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

program specification concurrent programs temporal logic finite model propositional branching time logic synchronisation skeleton tableau- based decision procedure

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25) Temporal logic (03B44)

Related Items

CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, A logical query language for hypermedia systems, \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers, The guarded fragment with transitive guards, Bounded situation calculus action theories, Not all bugs are created equal, but robust reachability can tell the difference, Model checking and abstraction to the aid of parameterized systems (a survey), A technique of state space search based on unfolding, Greening R. Thomas' framework with environment variables: a divide and conquer approach, Algebraic simulations, Deadlock in packet switching networks, Complexity of finite-variable fragments of propositional temporal and modal logics of computation, Determinization and memoryless winning strategies, Why there is no general solution to the problem of software verification, Ordered multi-stack visibly pushdown automata, Reasoning about equilibria in game-like concurrent systems, Question-guided stubborn set methods for state properties, A theoretical foundation of the DSSSL location model, Synthesis of communicating process skeletons from temporal-spatial logic specifications, Is my attack tree correct?, Formal modeling and verification for MVB, Characterizing finite Kripke structures in propositional temporal logic, Model-checking iterated games, A theory of formal synthesis via inductive learning, Branching-time logics with path relativisation, A complete axiomatization of weighted branching bisimulation, A complete proof system for propositional projection temporal logic, A temporal logic for real-time partial ordering with named transactions, An improved algorithm for the evaluation of fixpoint expressions, An accessible verification environment for UML models of services, On the semantics of strategy logic, Counting on CTL\(^*\): On the expressive power of monadic path logic, Synchronous counting and computational algorithm design, A complete axiom system for propositional projection temporal logic with cylinder computation model, Augmenting ATL with strategy contexts, Undecidable problems in unreliable computations., On feasible cases of checking multi-agent systems behavior., Verification of distributed systems with the axiomatic system of MSVL, A planner agent that tries its best in presence of nondeterminism, Reasoning about graded strategy quantifiers, Automated analysis of mutual exclusion algorithms using CCS, Verification of multi-linked heaps, Synthesis of Reactive(1) designs, Proof systems for satisfiability in Hennessy-Milner logic with recursion, Mathematical modal logic: A view of its evolution, Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning, Generating counterexamples for quantitative safety specifications in probabilistic B, Linear temporal logic symbolic model checking, Backdoors for linear temporal logic, Temporal logics for concurrent recursive programs: satisfiability and model checking, Refinement modal logic, Control machines: A new model of parallelism for compositional specifications and their effective compilation, Quantifier elimination by dependency sequents, Bounded semantics, TABLEAUX: A general theorem prover for modal logics, A hierarchy of temporal logics with past, About the expressive power of CTL combinators, Arity hierarchy for temporal logics, GR(1)*: GR(1) specifications extended with existential guarantees, On model checking multiple hybrid views, Verification of scope-dependent hierarchical state machines, Dependences in strategy logic, Alternating-time temporal logics with linear past, Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics, Inconsistency-tolerant temporal reasoning with hierarchical information, The modeling library of eavesdropping methods in quantum cryptography protocols by model checking, Assume-admissible synthesis, Mitigating covert channels based on analysis of the potential for communication, A hierarchy of failures-based models: theory and application, Relating fair testing and accordance for service replaceability, Weak Muller acceptance conditions for tree automata, Vacuity in practice: temporal antecedent failure, Producing explanations for rich logics, Test generation from P systems using model checking, Cycle detection in computation tree logic, An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation, One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\), Assume-guarantee synthesis for digital contract signing, Improving parity games in practice, A formal proof of the deadline driven scheduler in PPTL axiomatic system, Program repair without regret, A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria, Verification of reactive systems using temporal logic with clocks, Automatic symmetry detection for Promela, A multiprocess network logic with temporal and spatial modalities, Module checking, An infinite hierarchy of temporal logics over branching time, Results on the propositional \(\mu\)-calculus, Is your model checker on time? On the complexity of model checking for timed modal logics, Symbolic model checking of timed guarded commands using difference decision diagrams, Global and local views of state fairness, A taxonomy of fairness and temporal logic problems for Petri nets, Quantified computation tree logic, Clausal resolution in a logic of rational agency, Context-free timed formalisms: robust automata and linear temporal logics, Weak, strong, and strong cyclic planning via symbolic model checking, Translating Java for multiple model checkers: The Bandera back-end, Combining symmetry reduction and under-approximation for symbolic model checking, Language and communication problems in formalization: a natural language approach, Interpretability of first-order linear temporal logics in fork algebras, Model checking mobile ad hoc networks, An Algorithm for Probabilistic Alternating Simulation, On the universal and existential fragments of the \(\mu\)-calculus, Complexity results on branching-time pushdown model checking, Introduction to Model Checking, Model Checking Concurrent Programs, Combining Model Checking and Testing, Transfer of Model Checking to Industrial Practice, Functional Specification of Hardware via Temporal Logic, Graph Games and Reactive Synthesis, Process Algebra and Model Checking, The Complexity of Linear-Time Temporal Logic Model Repair, Structure-based deadlock checking of asynchronous circuits, On the Hybrid Extension of CTL and CTL +, Interleaving set temporal logic, Compositional Control Synthesis for Partially Observable Systems, Maintenance goals of agents in a dynamic environment: formulation and policy construction, Unnamed Item, Unnamed Item, Branching-time logics and fairness, revisited, Analyzing Oscillatory Behavior with Formal Methods, From model checking to equilibrium checking: reactive modules for rational verification, Dependences in Strategy Logic, Simulating and model checking membrane systems using strategies in Maude, Metalevel transformation of strategies, Unnamed Item, Mean-payoff games with \(\omega\)-regular specifications, A temporal logic for real-time partial-ordering with named transactions, rCOS: Defining Meanings of Component-Based Software Architectures, Formal Modelling, Analysis and Verification of Hybrid Systems, Enriched μ–Calculus Pushdown Module Checking, A CTL* Model Checker for Petri Nets, A survey on temporal logics for specifying and verifying real-time systems, Parameter space abstraction and unfolding semantics of discrete regulatory networks, Model checking and synthesis for branching multi-weighted logics, Efficiently Deciding μ-Calculus with Converse over Finite Trees, Generalized abstraction-refinement for game-based CTL lifted model checking, Model checking open systems with alternating projection temporal logic, Model checking of pushdown systems for projection temporal logic, A proof system for unified temporal logic, Distributed Synthesis for Alternating-Time Logics, The Birth of Model Checking, Discriminative Model Checking, A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, ATL* Satisfiability Is 2EXPTIME-Complete, Unnamed Item, Unnamed Item, Hierarchical cost-parity games, Unnamed Item, Unnamed Item, Model-checking precision agriculture logistics: the case of the differential harvest, Cancer hybrid automata: model, beliefs and therapy, Toward model selection by formal methods, Characteristic Formulae for Timed Automata, Algebra-based synthesis of loops and their invariants (invited paper), Generative program analysis and beyond: the power of domain-specific languages (invited paper), Model Checking Exact Cost for Attack Scenarios, Strategies, model checking and branching-time properties in Maude, Refinement of Synchronizable Places with Multi-workflow Nets, Code aware resource management, Model checking for probabilistic timed automata, Beyond vacuity: towards the strongest passing formula, Requirements, specifications, and minimal refinement, Observations in using parallel and sequential evolutionary algorithms for automatic software testing, Analysis of dynamic policies, Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol, Model Theoretic Syntax and Parsing, Unnamed Item, A clausal resolution method for extended computation tree logic ECTL, A parametric analysis of the state-explosion problem in model checking, On the order of test goals in specification-based testing, Tutorial on Model Checking: Modelling and Verification in Computer Science, \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\), From Philosophical to Industrial Logics, Model checking restricted sets of timed paths, ATL with Strategy Contexts and Bounded Memory, Synthesizing adaptive test strategies from temporal logic specifications, Statistical probabilistic model checking with a focus on time-bounded properties, Monitoring Metric First-Order Temporal Properties, Model-checking graded computation-tree logic with finite path semantics, Parameterized Complexity of CTL, Verifying untimed and timed aspects of the experimental batch plant, Natural strategic ability, Inferring Synchronization under Limited Observability, A novel approach to verifying context free properties of programs, Determinizing monitors for HML with recursion, Two AGM-style characterizations of model repair, Bounded model checking of traffic light control system, Logical vs. behavioural specifications, Aspect Categories and Classes of Temporal Properties, Weighted versus Probabilistic Logics, Branching-Time Temporal Logics with Minimal Model Quantifiers, On the Complexity of Branching-Time Logics, Solving Parity Games Using an Automata-Based Algorithm, Index set expressions can represent temporal logic formulas, The model checking fingerprints of CTL operators, Some Fixed-Point Issues in PPTL, Exogenous Probabilistic Computation Tree Logic, A goal-directed decision procedure for hybrid PDL, Next-preserving branching bisimulation, Unnamed Item, Partial-order reduction in the weak modal mu-calculus, Be lazy and don't care: faster CTL model checking for recursive state machines, Elimination of detached regions in dependency graph verification, Achieving high coverage in hardware equivalence checking via concolic verification, SMT-based verification of program changes through summary repair, On monitoring linear temporal properties, Machine learning and logic: a new frontier in artificial intelligence, Verification Modulo theories, Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic, Taming strategy logic: non-recurrent fragments, Revising system specifications in temporal logic, HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties, Probability logics for reasoning about quantum observations, Symbolic analysis of linear hybrid automata -- 25 years later, From interface automata to hypercontracts, Reasoning about Quality and Fuzziness of Strategic Behaviors, A Spatial Logic for Simplicial Models, A space-efficient on-the-fly algorithm for real-time model checking, Automated synthesis of asynchronizations, Symbolic computation in automated program reasoning, \textsf{PFL}: a probabilistic logic for fault trees, Taking Some Burden Off an Explicit CTL Model Checker, Computing sufficient and necessary conditions in CTL: a forgetting approach, Unnamed Item, From non-preemptive to preemptive scheduling using synchronization synthesis, Calculational design of a regular model checker by abstract interpretation, Modular Verification of Interactive Systems with an Application to Biology, A resolution calculus for the branching-time temporal logic CTL, Compositional Branching-Time Measurements, Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms, Model Checking Merged Program Traces, Proving the Refuted: Symbolic Model Checkers as Proof Generators, Smaller Abstractions for ∀CTL* without Next, Formal language properties of hybrid systems with strong resets, A Refined Resolution Calculus for CTL, Unnamed Item, From Monadic Logic to PSL, Approximation Refinement for Interpolation-Based Model Checking, The Complexity of CTL* + Linear Past, Unnamed Item, An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning, Automatically verifying temporal properties of pointer programs with cyclic proof, An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning, Unnamed Item, Hybrid linear logic, revisited, Model-Checking Counting Temporal Logics on Flat Structures