Reactive Systems

DOI10.1017/CBO9780511814105zbMath1141.68043OpenAlexW4252542281MaRDI QIDQ5309950

Luca Aceto, Anna Ingólfsdóttir, Jiří Srba, Kim Guldstrand Larsen

Publication date: 4 October 2007

Full work available at URL: https://doi.org/10.1017/cbo9780511814105

zbMATH Keywords

real-time systemsconcurrencytransition systemsprocess algebrasreactive systemsalgorithmic verificationHenessy-Milner logic

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Formal languages and automata (68Q45) Logic in computer science (03B70) 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 (54)

Characteristic formulae for fixed-point semantics: a general framework ⋮ Bidirectional Runtime Enforcement of First-Order Branching-Time Properties ⋮ Adequacy and complete axiomatization for timed modal logic ⋮ Dynamic Logic with Binders and Its Application to the Development of Reactive Systems ⋮ On the Executability of Interactive Computation ⋮ Monitorability for the Hennessy-Milner logic with recursion ⋮ Verification of finite-state machines: a distributed approach ⋮ When Are Prime Formulae Characteristic? ⋮ Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems ⋮ Synthesising correct concurrent runtime monitors ⋮ When are prime formulae characteristic? ⋮ On first-order runtime enforcement of branching-time properties ⋮ Simulation relations and applications in formal methods ⋮ Product line process theory ⋮ Testing interruptions in reactive systems ⋮ Bisimulations for fuzzy automata ⋮ Nondeterministic automata: equivalence, bisimulations, and uniform relations ⋮ Cyber-physical systems ⋮ Value-passing CCS with noisy channels ⋮ Unnamed Item ⋮ A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes ⋮ Unnamed Item ⋮ Reachability analysis for timed automata using max-plus algebra ⋮ Unnamed Item ⋮ Alternation-free weighted mu-calculus: decidability and completeness ⋮ Lattice-valued simulations for quantitative transition systems ⋮ Team bisimilarity, and its associated modal logic, for BPP nets ⋮ Compositional reasoning using intervals and time reversal ⋮ Computation of the greatest simulations and bisimulations between fuzzy automata ⋮ Differential privacy in probabilistic systems ⋮ An operational semantics for a calculus for wireless systems ⋮ Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations ⋮ Discount-Optimal Infinite Runs in Priced Timed Automata ⋮ Unnamed Item ⋮ Quantitative analysis of weighted transition systems ⋮ Teaching Concurrency Concepts to Freshmen ⋮ A logic for the stepwise development of reactive systems ⋮ On decidability of recursive weighted logics ⋮ Compositionality for quantitative specifications ⋮ Predicate liftings and functor presentations in coalgebraic expression languages ⋮ A linear-time-branching-time spectrum for behavioral specification theories ⋮ Determinizing monitors for HML with recursion ⋮ The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism ⋮ Bisimulation of type 2 for BL-general fuzzy automata ⋮ A theory of monitors ⋮ A study on team bisimulation and H-team bisimulation for BPP nets ⋮ Checking Timed Büchi Automata Emptiness Using LU-Abstractions ⋮ A propositional dynamic logic for instantial neighborhood semantics ⋮ Consistently-detecting monitors ⋮ CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions ⋮ Simplified Coalgebraic Trace Equivalence ⋮ Monitoring for Silent Actions ⋮ Simulation for lattice-valued doubly labeled transition systems ⋮ On bidirectional runtime enforcement

This page was built for publication: Reactive Systems