Executable Specifications in Transition Algebra

Abstract

Transition Algebra can be viewed as an extension of many-sorted first-order logic by borrowing essential features from dynamic logic. This leads us to new, more expressive sentences that include transitions labelled with actions, which are built from terms using union, composition, and iteration operators. We define a suitable notion of Horn clause, develop a system of proof rules for reasoning about clauses, and subsequently show that the proof system is sound and complete. We then introduce a rewriting relation based on Horn clauses, capturing transitions along established paths expressed as actions. This rewriting relation is naturally extended to a narrowing procedure for solving queries, thereby laying foundation for logic programming in Transition Algebra. As usual, soundness for both rewriting and narrowing is straightforward, whereas completeness requires additional conditions. Finally, we provide a prototype tool that demonstrates the practical aspects and shows the effectiveness of the proposed method.