Structural Refinement for the Modal nu-Calculus

DOI10.1007/978-3-319-10882-7_11MaRDI QIDQ2938159zbMATH OpenOpenAlexFDO

Authors Uli Fahrenberg, Axel Legay, Louis-Marie Traonouez

Publication date 13 January 2015

Published in Theoretical Aspects of Computing – ICTAC 2014 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1402.2143

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We introduce a new notion of structural refinement, a sound abstraction of logical implication, for the modal nu-calculus. Using new translations between the modal nu-calculus and disjunctive modal transition systems, we show that these two specification formalisms are structurally equivalent. Using our translations, we also transfer the structural operations of composition and quotient from disjunctive modal transition systems to the modal nu-calculus. This shows that the modal nu-calculus supports composition and decomposition of specifications.

Recommendations

• scientific article; zbMATH DE number 4131643
• A note on model checking the modal \(\nu\)-calculus
• scientific article; zbMATH DE number 6863637
• scientific article; zbMATH DE number 4187771
• Nested sequents for intuitionistic modal logics via structural refinement
• Refinement modal logic
• Modularisation of sequent calculi for normal and non-normal modalities
• scientific article; zbMATH DE number 1471992
• Decomposition theorems and model-checking for the modal \(\mu\)-calculus
• scientific article; zbMATH DE number 1136070

Cited in

(4)

• ACTL for modal interface automata
• Logical vs. behavioural specifications
• A linear-time-branching-time spectrum for behavioral specification theories
• Compositionality for quantitative specifications

This page was built for publication: Structural Refinement for the Modal nu-Calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938159)