On fork arrow logic and its expressive power (Q2454871)

Arrow logic is a modal logic used for reasoning about structures whose elements are arrows; therefore, it is closely related to relation algebras and algebras of nondeterministic processes (a relation being regarded as the input-output behaviour of a process). However, some features of processes, e.g. those concerning parallelism and synchronization, cannot be expressed in arrow logic. More generally, the expressive power of arrow logic is limited to a bounded fragment of first-order logic. Fork arrow logic is to fork algebras what arrow logic is to relation algebras. A fork algebra is a relation algebra equipped with a pairing function on the domain of relations, as well as an extra binary \textit{fork} operation on relations (see, e.g., the monograph [\textit{M. F. Frias}, Fork algebras in algebra, logic and computer science. Singapore: World Scientific (2002; Zbl 1012.03001)] for more details on fork algebras and fork logic -- a logic whose algebraic semantics is based on fork algebras). It is shown in the paper under review that every input-output behaviour expressible in first-order logic can also be expressed in fork arrow logic. From the introduction: ``This paper is structured as follows. Section 2 briefly reviews arrow logic under square semantics. Section 3 introduces ideas related to parallelism and coding and points out some limitations of arrow logic. Section 4 presents fork arrow logic. Section 5 establishes the expressive power of fork arrow logic. Section 6 presents some perspectives for further work.''