On fork arrow logic and its expressive power

DOI10.1007/S10992-006-9043-XMaRDI QIDQ2454871zbMATH OpenOpenAlexFDO

Authors Paulo A. S. Veloso, Renata P. de Freitas, Petrucio Viana, Sheila R. M. Veloso, Mario Benevides

Publication date 22 October 2007

Published in Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10992-006-9043-x

arrow logic expressive power first-order logic fork algebra modal logic process relation algebra

Modal logic (including the logic of norms) (03B45) Cylindric and polyadic algebras; relation algebras (03G15) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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.

Recommendations

Cites work

Cited in

(4)

This page was built for publication: On fork arrow logic and its expressive power

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2454871)