Counterpart Semantics for a Second-Order mu-Calculus

Research output: Contribution to journalJournal articlepeer-review

Abstract

Quantified mu-calculi combine the fix-point and modal operators of temporal logics with (existential and universal) quantifiers, and they allow for reasoning about the possible behaviour of individual components within a software system. In this paper we introduce a novel approach to the semantics of such calculi: we consider a sort of labeled transition systems called counterpart models as semantic domain, where states are algebras and transitions are defined by counterpart relations (a family of partial homomorphisms) between states. Then, formulae are interpreted over sets of state assignments (families of partial substitutions, associating formula variables to state components). Our proposal allows us to model and reason about the creation and deletion of components, as well as the merging of components. Moreover, it avoids the limitations of existing approaches, usually enforcing restrictions of the transition relation: the resulting semantics is a streamlined and intuitively appealing one, yet it is general enough to cover most of the alternative proposals we are aware of. The paper is rounded up with some considerations about expressiveness and decidability aspects.
Original languageEnglish
JournalFundamenta Informaticae
Volume118
Issue number1-2
Pages (from-to)177-205
Number of pages29
ISSN0169-2968
DOIs
Publication statusPublished - 2012
Externally publishedYes

Keywords

  • Biomineralization
  • Computability and decidability
  • Graph theory
  • Pathology
  • State assignment
  • Semantics
  • Graph Transformation
  • Individual components
  • Labeled transition systems
  • Modal logic
  • Modal operators
  • Partial substitution
  • Second orders
  • Semantic domains
  • Software systems
  • State component
  • Transition relations
  • counterpart semantics
  • graph transformation
  • modal logics
  • Quantified μ-calculi
  • COMPUTER
  • MATHEMATICS,
  • SPATIAL LOGIC
  • PI-CALCULUS
  • TEMPORAL LOGIC
  • GRAPH LOGIC
  • VERIFICATION
  • LANGUAGE
  • Quantified mu-calculi

Fingerprint

Dive into the research topics of 'Counterpart Semantics for a Second-Order mu-Calculus'. Together they form a unique fingerprint.

Cite this