================================================================================
P9308   J.F.A.K. van Benthem & J.A. Bergstra
        "Logic of transition systems"


Labeled transition systems are key structures for modeling computation. In
this paper, we show how they lend themselves to ordinary logical analysis
(without any special new formalisms), by introducing their standard
first-order theory. This perspective enables us to raise several basic
model-theoretic questions of definability, axiomatization and preservation
for various notions of process equivalence found in the computational
literature, and answer them using well-known logical techniques (including
the Compactness theorem, Saturation, and Ehrenfeucht games). Moreover, we
consider what happens to this general theory when one restricts attention
to special classes of transition systems (in particular, finite ones), as
well as extended logical languages (in particular, infinitary first-order
logic). We hope that this puts standard logical formalisms on the map as a
serious option for a theory of computational processes. As a side benefit,
our approach increases comparability with several other existing formalisms
over labeled transition systems (such as Process Algebra or Modal Logic).
We provide some pointers to this effect, too.