Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions

Hennicker, Rolf; Knapp, Alexander; Madeira, Alexandre und Mindt, Felix (2020): Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions. In: Dynamic Logic: New Trends and Applications, Dali 2019, Bd. 12005: S. 19-34

Abstract

We extend dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations of the logic: abstractor and behavioural specifications. Abstractor specifications relax the standard model class semantics of a specification by considering its closure under weak bisimulation. Behavioural specifications, however, rely on a behavioural satisfaction relation which relaxes the interpretation of state variables and the satisfaction of modal formulas <alpha >phi and [alpha]phi by abstracting from silent transitions. A formal relation between abstractor and behavioural specifications is provided which shows that both coincide semantically under mild conditions. For the proof we instantiate the previously introduced concept of a behaviour-abstractor framework to the case of dynamic logic with binders and silent transitions.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0302-9743
• Sprache: Englisch