Characteristic Formulae for Relations with Nested Fixed Points

TL;DR

This paper extends the framework connecting characteristic formulae and behavioral semantics to cover nested fixed points, enabling analysis of more complex semantics like n-nested simulation.

Contribution

It introduces a novel description of nested fixed points that generalizes existing methods for single fixed points, filling a key gap in the theory.

Findings

Extended the characteristic formula framework to nested fixed points

Provided an intuitive and comprehensive description for nested fixed points

Enhanced the applicability of the framework to complex semantics like n-nested simulation

Abstract

A general framework for the connection between characteristic formulae and behavioral semantics is described in [2]. This approach does not suitably cover semantics defined by nested fixed points, such as the n-nested simulation semantics for n greater than 2. In this study we address this deficiency and give a description of nested fixed points that extends the approach for single fixed points in an intuitive and comprehensive way.