Characteristic formulae for fixed-point semantics: a general framework

DOI10.1017/S0960129511000375zbMath1279.68181OpenAlexW2113617913MaRDI QIDQ2883115

Anna Ingólfsdóttir, Luca Aceto, Paul Blain Levy, Joshua Sack

Publication date: 11 May 2012

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (8)

A General Framework for Probabilistic Characterizing Formulae ⋮ Logical characterisations, rule formats and compositionality for input-output conformance simulation ⋮ Removing redundant refusals: minimal complete test suites for failure trace semantics ⋮ The complexity of identifying characteristic formulae ⋮ On recursive operations over logic LTS ⋮ Logical characterization of branching metrics for nondeterministic probabilistic transition systems ⋮ Unnamed Item ⋮ Encoding safety in \(\mathrm{CLL}_R\)

Cites Work

• Modal logics for communicating systems
• Graphical versus logical specifications
• Results on the propositional \(\mu\)-calculus
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• Characterizing finite Kripke structures in propositional temporal logic
• Bisimulation through probabilistic testing
• Structured operational semantics and bisimulation as a congruence
• Modal correspondence for models
• Characteristic formulae for processes with divergence
• A note on graded modal logic
• Finite models constructed from canonical formulas
• A general approach to comparing infinite-state systems with their finite-state specifications
• A lattice-theoretical fixpoint theorem and its applications
• Characteristic Formulae for Timed Automata
• Non-strongly Stable Orders Also Define Interesting Simulation Relations
• From timed automata to logic — and back
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• A modal characterization of observational congruence on finite terms of CCS
• Algebraic laws for nondeterminism and concurrency
• Formal verification of parallel programs
• Termination, deadlock, and divergence
• Bisimulation can't be traced
• Three logics for branching bisimulation
• Branching time and abstraction in bisimulation semantics
• Reactive Systems

This page was built for publication: Characteristic formulae for fixed-point semantics: a general framework