scientific article

Publication date: 18 September 1992

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

temporal logic concurrency formal specification of reactive systems

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

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

Reactive computing as model generation ⋮ Detecting causal relationships in distributed computations: In search of the holy grail ⋮ A fully abstract trace model for dataflow and asynchronous networks ⋮ Model checking and abstraction to the aid of parameterized systems (a survey) ⋮ Spanning the spectrum from safety to liveness ⋮ Quantitative solution of omega-regular games ⋮ Safety, liveness and fairness in temporal logic ⋮ A principle for sequential reasoning about distributed algorithms ⋮ Beyond contracts for concurrency ⋮ Synthesis with rational environments ⋮ On the diversity of asynchronous communication ⋮ First-order temporal verification in practice ⋮ Coverage metrics for temporal logic model checking ⋮ Modeling data-intensive reactive systems with relational transition systems ⋮ On control of systems modelled as deterministic Rabin automata ⋮ Interpreting message flow graphs ⋮ Tightening the contract refinements of a system architecture ⋮ A mathematical framework for the semantics of symbolic languages representing periodic time ⋮ Hybridization methods for the analysis of nonlinear systems ⋮ Finite-trace linear temporal logic: coinductive completeness ⋮ Duration calculus: Logical foundations ⋮ Compositional verification of real-time systems with explicit clock temporal logic ⋮ Verifying a signature architecture: a comparative case study ⋮ Specification and verification of data-driven Web applications ⋮ MAVEN: Modular aspect verification and interference analysis ⋮ Early verification and validation of mission critical systems ⋮ A criterion for atomicity revisited ⋮ A complete proof system for propositional projection temporal logic ⋮ Planning control rules for reactive agents ⋮ Preface to the special issue: Temporal logics of agency ⋮ On feasible cases of checking multi-agent systems behavior. ⋮ Nontransitive temporal multiagent logic, information and knowledge, deciding algorithms ⋮ Verification of distributed systems with the axiomatic system of MSVL ⋮ Pointfree expression and calculation: From quantification to temporal logic ⋮ Correct transformation: from object-based graph grammars to PROMELA ⋮ Aspects preserving properties ⋮ Lock-free dynamic hash tables with open addressing ⋮ Fault-containing self-stabilizing distributed protocols ⋮ Completeness of temporal logics over infinite intervals. ⋮ Explaining counterexamples using causality ⋮ Formal communication elimination and sequentialization equivalence proofs for distributed system models ⋮ Exploring the boundary of half-positionality ⋮ Branching time logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha }\) with operations \textit{Until} and \textit{Since} based on bundles of integer numbers, logical consecutions, deciding algorithms ⋮ Runtime verification of embedded real-time systems ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Deductive verification of alternating systems ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ Finite divergence ⋮ Sequential calculus ⋮ Component-wise incremental LTL model checking ⋮ Organising LTL monitors over distributed systems with a global clock ⋮ On the axiomatizability of some first-order spatio-temporal theories ⋮ Partial-order Boolean games: informational independence in a logic-based model of strategic interaction ⋮ A symbolic model for timed concurrent constraint programming ⋮ Faster algorithms for mean-payoff games ⋮ A formal approach for the construction and verification of railway control systems ⋮ Decidability of infinite-state timed CCP processes and first-order LTL ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ Deriving non-zeno behaviour models from goal models using ILP ⋮ Property specifications for workflow modelling ⋮ A compositional approach to CTL\(^*\) verification ⋮ Fairness of transitions in diagnosability of discrete event systems ⋮ Linear time-dependent constraints programming with MSVL ⋮ On stubborn sets in the verification of linear time temporal properties ⋮ IPL: an integration property language for multi-model cyber-physical systems ⋮ Reconciling statechart semantics ⋮ A general technique for proving lock-freedom ⋮ Reasoning about goal-directed real-time teleo-reactive programs ⋮ Assume-guarantee synthesis for digital contract signing ⋮ Time and logic: A calculus of binary events ⋮ Progress assumption in concurrent systems ⋮ Tool support for learning Büchi automata and linear temporal logic ⋮ Decidability results for metric and layered temporal logics ⋮ Partitioned PLTL model-checking for refined transition systems ⋮ Event-clock automata: a determinizable class of timed automata ⋮ Proving possibility properties ⋮ On the refinement of liveness properties of distributed systems ⋮ Quantitatively fair scheduling ⋮ Multimedia data modeling based on temporal logic and \(XYZ\) system ⋮ From liveness to promptness ⋮ Systems of agents controlled by logical programs: complexity of verification ⋮ Distributed automata in an assumption-commitment framework ⋮ Deductive verification of real-time systems using STeP ⋮ Verification, refinement and scheduling of real-time programs ⋮ Correctness of substring-preprocessing in Boyer-Moore's pattern matching algorithm ⋮ Testing preorders for probabilistic processes. ⋮ A timed concurrent constraint language. ⋮ Verification by augmented finitary abstraction ⋮ Module checking ⋮ On the complexity of verifying concurrent transition systems ⋮ The complexity of propositional linear temporal logics in simple cases ⋮ Truly concurrent constraint programming ⋮ Network event recognition ⋮ Algebraic specification of agent computation ⋮ Models for reactivity ⋮ Querying datalog programs with temporal logic ⋮ Translating Java for multiple model checkers: The Bandera back-end ⋮ A complete mechanization of correctness of a string-preprocessing algorithm ⋮ An equivalent CTL formulation for condition sequences ⋮ Interpretability of first-order linear temporal logics in fork algebras

This page was built for publication: