Dynamic logic assigned to automata

TL;DR

This paper introduces a dynamic logic framework applicable to all automata, deterministic or nondeterministic, allowing for the formulation of observations and capturing their dynamic behavior through a transition functor.

Contribution

It presents a novel dynamic logic assigned to automata that enables analysis of their behavior and conditions for automaton recovery from the logic and transition functor.

Findings

Logic applies to both deterministic and nondeterministic automata

Formulates conditions for automaton recovery from logic and transition functor

Captures automaton dynamics through a transition functor

Abstract

A dynamic logic ${\mathbf B}$ can be assigned to every automaton ${\mathcal A}$ without regard if ${\mathcal A}$ is deterministic or nondeterministic. This logic enables us to formulate observations on ${\mathcal A}$ in the form of composed propositions and, due to a transition functor $T$, it captures the dynamic behaviour of ${\mathcal A}$. There are formulated conditions under which the automaton ${\mathcal A}$ can be recovered by means of ${\mathbf B}$ and $T$.