Abstract
Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work [9] on the systematic generation of dynamic logics from the propositional to the equational case, to capture ‘full-fledged’ imperative programs. The generation process is parametric on a structure specifying a notion of ‘weight’ assigned to programs. The paper introduces also a notion of bisimilarity on models of the generated logics, which is shown to entail modal equivalence with respect to the latter. © 2019, Springer Nature Switzerland AG.

Abstract
This paper introduces a sort of automata and associated languages, often arising in modelling natural phenomena, in which both vagueness and simultaneity are taken as first class citizens. This requires a fuzzy semantics assigned to transitions and a precise notion of a synchronous product to enforce the simultaneous occurrence of actions. The expected relationships between automata and languages are revisited in this setting; in particular it is shown that any subset of a fuzzy synchronous language with the suitable signature forms a synchronous Kleene algebra.

Abstract
This note, reporting the homonym keynote presented in the International Symposium on Molecular Logic and Computational Synthetic Biology 2018, traces an informal roadmap on Dynamic Logic (DL) field, focusing on its versatility and resilience to be adjusted and adopted in a wide class of application domains and computational paradigms. The exposition argues the room for developments on tagging DL to the analysis of synthetic biologic domain. © 2019, Springer Nature Switzerland AG.

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 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.

Abstract
This paper intends to contribute with a new fuzzy modal logic to model and reason about transition systems involving uncertainty in behaviours. Our formalism supports fuzziness at transitions and on the proposition symbols assignment levels. Against of other approaches in the literature, our bisimulation and bisimilarity notions generalise the analogous standard notions of classic modal logic and of process algebras. Moreover, the outcome of our logic is also fuzzy, with the semantic interpretation of connectives supported by the Godel algebra.

Abstract