Theory Energy
section ‹Expressiveness Prices›
theory Energy
imports "HOL-Library.Extended_Nat"
begin
text ‹
We intend to work on eight-dimensional vectors in an energy game.
The dimensions will encode expressiveness prices to HML$_\text{SRBB}$ formulas.
This price is supposed to capture syntactic features needed to describe a certain property and will later be used to select sublogics of specific expressiveness to characterize behavioural equivalences.
The eight dimensions are intended to measure the following properties of formulas:
▸ Modal depth (of observations $\langle\alpha\rangle$, $(\alpha)$),
▸ Depth of branching conjunctions (with one observation clause not starting with $\langle\varepsilon\rangle$),
▸ Depth of stable conjunctions (that do enforce stability by a $\neg\langle\tau\rangle\top$-conjunct),
▸ Depth of unstable conjunctions (that do not enforce stability by a $\neg\langle\tau\rangle\top$-conjunct),
▸ Depth of immediate conjunctions (that are not preceded by $\langle\varepsilon\rangle$),
▸ Maximal modal depth of positive clauses in conjunctions,
▸ Maximal modal depth of negative clauses in conjunctions,
▸ Depth of negations
›