On fork arrow logic and its expressive power

We compare fork arrow logic, an extension of arrow logic, and its natural first-order counterpart (the correspondence language) and show that both have the same expressive power. Arrow logic is a modal logic for reasoning about arrow structures, its expressive power is limited to a bounded fragment of first-order logic. Fork arrow logic is obtained by adding to arrow logic the fork modality (related to parallelism and synchronization). As a result, fork arrow logic attains the expressive power of its first-order correspondence language, so both can express the same input–output behavior of processes.