Logo Logo
Hilfe
Hilfe
Switch Language to English

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

Volltext auf 'Open Access LMU' nicht verfügbar.

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.

Dokument bearbeiten Dokument bearbeiten