On Recursive Operations Over Logic LTS

TL;DR

This paper develops a theoretical framework for recursive operations over Logic LTS, establishing fundamental properties like precongruence and solution uniqueness in a process-algebraic style.

Contribution

It introduces a general theory for nested recursive operations over Logic LTS, addressing open problems and establishing key properties.

Findings

Precongruence of recursive operations

Uniqueness of consistent solutions for equations

Framework unifies algebraic and logical specification styles

Abstract

Recently, in order to mix algebraic and logic styles of specification in a uniform framework, the notion of a logic labelled transition system (Logic LTS or LLTS for short) has been introduced and explored. A variety of constructors over LLTS, including usual process-algebraic operators, logic connectives (conjunction and disjunction) and standard temporal operators (always and unless), have been given. However, no attempt has made so far to develop general theory concerning (nested) recursive operations over LLTSs and a few fundamental problems are still open. This paper intends to study this issue in pure process-algebraic style. A few fundamental properties, including precongruence and the uniqueness of consistent solutions for equations, will be established.