Characteristic formulae for processes with divergence
From MaRDI portal
Publication:1322469
DOI10.1006/inco.1994.1028zbMath0804.68097OpenAlexW2025280888MaRDI QIDQ1322469
Bernhard Steffen, Anna Ingólfsdóttir
Publication date: 5 May 1994
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.1994.1028
model checkingbisimulationtransition systemsHennessy-Milner logicmutual recursiondivergence information
Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items
Characteristic formulae for fixed-point semantics: a general framework, Unifying models, Verifying persistent security properties, When Are Prime Formulae Characteristic?, Characteristic invariants in Hennessy-Milner logic, When are prime formulae characteristic?, The power of reachability testing for timed automata, Logical characterisations, rule formats and compositionality for input-output conformance simulation, The complexity of bisimilarity-checking for one-counter processes., Removing redundant refusals: minimal complete test suites for failure trace semantics, Characteristic Formulae for Timed Automata, The complexity of identifying characteristic formulae, Complete proof systems for weighted modal logic, Event Identifier Logic, Deciding bisimulation-like equivalences with finite-state processes, Logical characterization of branching metrics for nondeterministic probabilistic transition systems, A general approach to comparing infinite-state systems with their finite-state specifications, Connection between logical and algebraic approaches to concurrent systems, Predicate liftings and functor presentations in coalgebraic expression languages, Encoding safety in \(\mathrm{CLL}_R\), Reasoning about nondeterministic and concurrent actions: A process algebra approach, A Logical Process Calculus, Unnamed Item, Property-oriented expansion
