On Recursive Operations Over Logic LTS
This work addresses foundational gaps in formal methods for researchers in process algebra and logic specification, but it is incremental as it builds on existing LLTS frameworks.
The paper tackles the lack of a general theory for recursive operations over logic labelled transition systems (LLTS) by establishing fundamental properties such as precongruence and uniqueness of consistent solutions for equations in a process-algebraic style.
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.