From c483053a85c0db4c698e82445b4dd91a3c088ad6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 28 May 2011 15:22:12 +0200 Subject: [PATCH] Add documentation for temporal logic operators. * doc/tl/Makefile.am, doc/tl/tl.tex, doc/tl/tl.bib: New files. * doc/Makefile.am (SUBDIRS): Recurse into tl/. * configure.ac: Output doc/tl/Makefile * README: Describe doc/tl/. --- README | 3 +- configure.ac | 1 + doc/Makefile.am | 4 +- doc/tl/.gitignore | 6 + doc/tl/Makefile.am | 33 ++ doc/tl/tl.bib | 101 ++++ doc/tl/tl.tex | 1404 ++++++++++++++++++++++++++++++++++++++++++++ 7 files changed, 1550 insertions(+), 2 deletions(-) create mode 100644 doc/tl/.gitignore create mode 100644 doc/tl/Makefile.am create mode 100644 doc/tl/tl.bib create mode 100644 doc/tl/tl.tex diff --git a/README b/README index c4492bfbb..f25dee5ed 100644 --- a/README +++ b/README @@ -143,7 +143,8 @@ src/ Sources for libspot. neverparse/ Parser for SPIN never claims. sanity/ Sanity tests for the whole project. doc/ Documentation for libspot. - spot.html/ HTML reference manual. + tl/ Documentation of the Temporal Logic operators. + spot.html/ HTML reference manual for the library. bench/ Benchmarks for ... emptchk/ ... emptiness-check algorithms, gspn-ssp/ ... various symmetry-based methods with GreatSPN, diff --git a/configure.ac b/configure.ac index 92d9712f8..24d3dc35d 100644 --- a/configure.ac +++ b/configure.ac @@ -118,6 +118,7 @@ AC_CONFIG_FILES([ bench/wdba/defs doc/Doxyfile doc/Makefile + doc/tl/Makefile iface/dve2/defs iface/dve2/Makefile iface/gspn/defs diff --git a/doc/Makefile.am b/doc/Makefile.am index 05e6a5a01..3002f4ac6 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -23,6 +23,8 @@ DOXYGEN = doxygen +SUBDIRS = tl + .PHONY: doc fast-doc all-local: $(srcdir)/stamp @@ -52,4 +54,4 @@ EXTRA_DIST = \ footer.html \ mainpage.dox \ $(srcdir)/stamp \ - $(srcdir)/spot.html \ No newline at end of file + $(srcdir)/spot.html diff --git a/doc/tl/.gitignore b/doc/tl/.gitignore new file mode 100644 index 000000000..27bf2858c --- /dev/null +++ b/doc/tl/.gitignore @@ -0,0 +1,6 @@ +*.bbl +*.blg +*.idx +*.log +*.out +tmp.t2d diff --git a/doc/tl/Makefile.am b/doc/tl/Makefile.am new file mode 100644 index 000000000..c4d3df8a1 --- /dev/null +++ b/doc/tl/Makefile.am @@ -0,0 +1,33 @@ +## Copyright (C) 2011 Laboratoire de Recherche et Développement de +## l'Epita (LRDE). +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + + +all: $(srcdir)/tl.pdf +TEXI2PDF = texi2dvi --pdf +TEXI2PDF_FLAGS = --tidy --build-dir=tmp.t2d --batch + +dist_pdf_DATA = $(srcdir)/tl.pdf + +$(srcdir)/tl.pdf: $(srcdir)/tl.tex $(srcdir)/tl.bib + $(TEXI2PDF) $(TEXI2PDF_FLAGS) -o $@ $< + +.PHONY: mostlyclean-local +mostlyclean-local: + rm -rf tmp.t2d diff --git a/doc/tl/tl.bib b/doc/tl/tl.bib new file mode 100644 index 000000000..43f455a5c --- /dev/null +++ b/doc/tl/tl.bib @@ -0,0 +1,101 @@ +@InProceedings{ somenzi.00.cav, + author = {Fabio Somenzi and Roderick Bloem}, + title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, + booktitle = {Proceedings of the 12th International Conference on + Computer Aided Verification (CAV'00)}, + pages = {247--263}, + year = {2000}, + volume = {1855}, + series = {Lecture Notes in Computer Science}, + address = {Chicago, Illinois, USA}, + publisher = {Springer-Verlag} +} + +@InProceedings{ etessami.00.concur, + author = {Kousha Etessami and Gerard J. Holzmann}, + title = {Optimizing {B\"u}chi Automata}, + booktitle = {Proceedings of the 11th International Conference on + Concurrency Theory (Concur'00)}, + pages = {153--167}, + year = {2000}, + editor = {C. Palamidessi}, + volume = {1877}, + series = {Lecture Notes in Computer Science}, + address = {Pennsylvania, USA}, + publisher = {Springer-Verlag}, + note = {Beware of a typo in the version from the + proceedings: $f \U g$ is purely eventual if both + operands are purely eventual. The revision of the + paper available at + \url{http://www.bell-labs.com/project/TMP/} is + fixed. We fixed the bug in Spot in 2005, thanks to + LBTT. See also \url{http://arxiv.org/abs/1011.4214v2} + for a discussion about this problem.} +} + +@InProceedings{manna.87.podc, + author = {Zohar Manna and Amir Pnueli}, + title = {A hierarchy of temporal properties}, + booktitle = {Proceedings of the sixth annual ACM Symposium on Principles of distributed computing (PODC'90)}, + year = {1990}, + location = {Quebec City, Canada}, + pages = {377--410}, + publisher = {ACM}, + address = {New York, NY, USA}, +} + +@InProceedings{ chang.92.icalp, + author = {Edward Y. Chang and Zohar Manna and Amir Pnueli}, + title = {Characterization of Temporal Property Classes}, + booktitle = {Proceedings of the 19th International Colloquium on + Automata, Languages and Programming (ICALP'92)}, + year = {1992}, + pages = {474--486}, + publisher = {Springer-Verlag}, + address = {London, UK} +} + +@InProceedings{ cerna.03.mfcs, + author = {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek}, + title = {Relating Hierarchy of Temporal Properties to Model + Checking}, + booktitle = {Proceedings of the 28th International Symposium on + Mathematical Foundations of Computer Science (MFCS'03)}, + pages = {318--327}, + year = {2003}, + editor = {Branislav Rovan and Peter Vojt{\'a}{\v{a}}}, + volume = {2747}, + series = {Lecture Notes in Computer Science}, + address = {Bratislava, Slovak Republic}, + month = aug, + publisher = {Springer-Verlag} +} + +@InProceedings{ schneider.01.lpar, + author = {Klaus Schneider}, + title = {Improving Automata Generation for Linear Temporal Logic by + Considering the Automaton Hierarchy}, + booktitle = {Proceedings of the 8th International Conference on Logic + for Programming, Artificial Intelligence and Reasoning}, + pages = {39--54}, + year = {2001}, + volume = {2250}, + series = {Lecture Notes in Artificial Intelligence}, + address = {Havana, Cuba}, + publisher = {Springer-Verlag} +} + +@TechReport{ tauriainen.03.a83, + author = {Heikki Tauriainen}, + title = {On Translating Linear Temporal Logic into Alternating and + Nondeterministic Automata}, + institution = {Helsinki University of Technology, Laboratory for + Theoretical Computer Science}, + address = {Espoo, Finland}, + month = dec, + number = {A83}, + pages = {132}, + type = {Research Report}, + year = {2003}, + note = {Reprint of Licentiate's thesis} +} diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex new file mode 100644 index 000000000..f5261fd0b --- /dev/null +++ b/doc/tl/tl.tex @@ -0,0 +1,1404 @@ +\RequirePackage[l2tabu, orthodox]{nag} +\documentclass[a4paper,twoside,10pt,DIV=12,draft]{scrreprt} +\usepackage[stretch=10]{microtype} +\usepackage[american]{babel} +\usepackage[latin1]{inputenc} +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage[sc]{mathpazo} +\usepackage{hyperref} +\usepackage{url} +\usepackage{xspace} +\usepackage{dsfont} +\usepackage{mathabx} +\usepackage{showlabels} +\usepackage{chngpage} +\usepackage{tabulary} +\usepackage[numbers]{natbib} +\usepackage{rotating} + +% TODO +\usepackage{todonotes} +\newcommand{\stodo}[2][] + {\todo[caption={#2},#1] + {\footnotesize #2}} +\newcommand{\spottodo}[2][]{\stodo[color=green!40,caption={#2},#1]{#2}} +\newcommand{\ltltodo}[2][]{\stodo[color=red!40,caption={#2},#1]{#2}} + + +%% ---------------------- %% +%% Mathematical symbols. %% +%% ---------------------- %% +\newcommand{\Z}{\texorpdfstring{\ensuremath{\mathds{Z}}}{Z}} +\newcommand{\B}{\texorpdfstring{\ensuremath{\mathds{B}}}{B}} +\newcommand{\N}{\texorpdfstring{\ensuremath{\mathds{N}}}{N}} +\newcommand{\AP}{\ensuremath{\mathrm{AP}}} + +\DeclareMathOperator{\F}{\texttt{F}} +\DeclareMathOperator{\FALT}{\texttt{<>}} +\DeclareMathOperator{\G}{\texttt{G}} +\DeclareMathOperator{\GALT}{\texttt{[]}} +\newcommand{\U}{\mathbin{\texttt{U}}} +\newcommand{\R}{\mathbin{\texttt{R}}} +\newcommand{\RALT}{\mathbin{\texttt{V}}} +\DeclareMathOperator{\X}{\texttt{X}} +\DeclareMathOperator{\XALT}{\texttt{()}} +\newcommand{\M}{\mathbin{\texttt{M}}} +\newcommand{\W}{\mathbin{\texttt{W}}} +\DeclareMathOperator{\NOT}{\texttt{!}} +\DeclareMathOperator{\NOTALT}{\texttt{\char`~}} +\newcommand{\XOR}{\mathbin{\texttt{xor}}} +\newcommand{\XORALT}{\mathbin{\texttt{\char`^}}} +\newcommand{\IMPLIES}{\mathbin{\texttt{->}}} +\newcommand{\IMPLIESALT}{\mathbin{\texttt{=>}}} +\newcommand{\IMPLIESALTT}{\mathbin{\texttt{-->}}} +\newcommand{\EQUIV}{\mathbin{\texttt{<->}}} +\newcommand{\EQUIVALT}{\mathbin{\texttt{<=>}}} +\newcommand{\EQUIVALTT}{\mathbin{\texttt{<-->}}} +\newcommand{\OR}{\mathbin{\texttt{|}}} +\newcommand{\ORALT}{\mathbin{\texttt{||}}} +\newcommand{\ORALTT}{\mathbin{\texttt{\char`\\/}}} +\newcommand{\AND}{\mathbin{\texttt{\&}}} +\newcommand{\ANDALT}{\mathbin{\texttt{\&\&}}} +\newcommand{\ANDALTT}{\mathbin{\texttt{/\char`\\}}} +\newcommand{\FUSION}{\mathbin{\texttt{:}}} +\newcommand{\CONCAT}{\mathbin{\texttt{;}}} +\newcommand{\0}{\texttt{0}} +\newcommand{\1}{\texttt{1}} +\newcommand{\STAR}[1]{\texttt{[*#1]}} +\newcommand{\STARALT}{\texttt{*}} +\newcommand{\EQUAL}[1]{\texttt{[=#1]}} +\newcommand{\GOTO}[1]{\texttt{[->#1]}} +\newcommand{\PLUS}{\texttt{[+]}} +\newcommand{\eword}{\texttt{[*0]}} + +\newcommand{\Esuffix}{\texttt{<>->}} +\newcommand{\EsuffixMarked}{\texttt{<>+>}} +\newcommand{\Asuffix}{\texttt{[]->}} +\newcommand{\AsuffixALT}{\texttt{|->}} +\newcommand{\EsuffixEQ}{\texttt{<>=>}} +\newcommand{\AsuffixEQ}{\texttt{[]=>}} +\newcommand{\AsuffixALTEQ}{\texttt{|=>}} + +\newcommand{\ratgroup}[1]{\texttt{\{}#1\texttt{\}}} +\newcommand{\nratgroup}[1]{\texttt{!\{}#1\texttt{\}}} +\newcommand{\ratgroupn}[1]{\texttt{\{}#1\texttt{\}!}} + +\def\limplies{\rightarrow} +\def\simp{\rightrightharpoons} +\def\Simp{\stackrel{+}{\simp}} +\def\liff{\leftrightarrow} + +\makeatletter +\newcommand{\Cxx}{% + \valign{\vfil\hbox{##}\vfil\cr + {C\kern-.1em}\cr + $\hbox{\fontsize\sf@size\z@\textbf{+\kern-0.05em+}}$\cr}% + \xspace +} +\makeatother + +\def\clap#1{\hbox to 0pt{\hss#1\hss}} +\def\mathllap{\mathpalette\mathllapinternal} +\def\mathrlap{\mathpalette\mathrlapinternal} +\def\mathclap{\mathpalette\mathclapinternal} +\def\mathllapinternal#1#2{% + \llap{$\mathsurround=0pt#1{#2}$}} +\def\mathrlapinternal#1#2{% + \rlap{$\mathsurround=0pt#1{#2}$}} +\def\mathclapinternal#1#2{% + \clap{$\mathsurround=0pt#1{#2}$}} + +% The same argument is output and put in the index. +\usepackage{makeidx} +\makeindex +\newcommand{\Index}[1]{\index{#1}#1} + + +% @SpotVersion@ +\def\SpotVersion{0.7.1a} + +%% ----------------------- %% +%% Texinfo like commands. %% +%% ----------------------- %% + +\newcommand\file[1]{`\texttt{#1}'} +\newcommand\command[1]{\texttt{#1}} +\newcommand\var[1]{{\ttfamily\itshape #1}} +\newcommand\mvar[1]{\ensuremath{\mathit{#1}}} +\newcommand\code[1]{\texttt{#1}} +\newcommand\samp[1]{`\texttt{#1}'} +\newcommand\tsamp[1]{\text{\texttt{#1}}} +\newcommand\msamp[1]{#1} + + +\def\manualtitle{Spot's Temporal Logic Formul\ae} + +%% ---------- %% +%% Document. %% +%% ---------- %% +\begin{document} + +\vspace*{50pt} +\vskip4pt \hrule height 4pt width \hsize \vskip4pt +\begin{center} + \huge \manualtitle +\end{center} +\vspace*{-1.5ex} +\vskip4pt \hrule height 4pt width \hsize \vskip4pt + +\hfill Alexandre Duret-Lutz +\href{mailto:adl@lrde.epita.fr}{\nolinkurl{}} + +\hfill compiled on \today, for Spot \SpotVersion + +\vfill + +\setcounter{tocdepth}{2} +\makeatletter +\@starttoc{toc} +\makeatother + +\vfill + +\chapter{Reasoning with Infinite Sequences} + +\section{Finite and Infinite Sequences} + +Let $\N=\{0,1,2,\ldots\}$ designate the set of natural numbers and +$\omega\not\in\N$ the first transfinite ordinal. We extend the $<$ +relation from $\N$ to $\N\cup\{\omega\}$ with $\forall n\in N,\, +n<\omega$. Similarly let us extend the addition and subtraction with +$\forall n\in\N,\,\omega+n = \omega-n = \omega+\omega = \omega$. + +For any set $A$, and any number $n\in\N\cup\{\omega\}$, a +\textit{sequence} of length $n$ is a function $\sigma: +\{0,1,\ldots,n-1\}\to A$ that associates each index $i} operators. + +\begin{align*} + \NOT \0 &\equiv \1 & + \1\IMPLIES f &\equiv f & + f\IMPLIES\1 &\equiv \1 \\ + \NOT\1 &\equiv \0 & + \0\IMPLIES f &\equiv \1& + f \IMPLIES 0 &\equiv \NOT f \\ + \NOT\NOT f &\equiv f & + && f\IMPLIES f &\equiv \1 +\end{align*} + +The next set of rules apply to operators that are commutative, so +these identities are also valid with the two arguments swapped. + +\begin{align*} + \0\AND f &\equiv \0 & + \0\OR f &\equiv f& + \0\XOR f &\equiv f & + \0\EQUIV f &\equiv \NOT f \\ + \1\AND f &\equiv f & + \1\OR f &\equiv \1 & + \1\XOR f &\equiv \NOT f& + \1\EQUIV f &\equiv f \\ + f\AND f &\equiv f & + f\OR f &\equiv f & + f\XOR f &\equiv \0& + f\EQUIV f &\equiv \1 +\end{align*} + +The \samp{\&} and \samp{|} operators are associative, so they are +actually implemented as $n$-ary operators (i.e., not binary): this +allows us to reorder all arguments in a unique way +(e.g. alphabetically). For instance the two expressions +\samp{a\&c\&b\&!d} and \samp{c\&!d\&b\&a} are actually represented as +the operator \samp{\&} applied to the arguments +$\{\code{a},\code{b},\code{c},\code{!d}\}$. Because these two +expressions have the same internal representation, they are actually +considered equal for the purpose of the above identities. For +instance \samp{(a\&c\&b\&!d)->(c\&!d\&b\&a)} will be rewritten to +\samp{1} automatically. + +\subsection{Unabbreviations}\label{sec:unabbbool} + +The `\verb=unabbreviate_logic_visitor=' rewrites all Boolean operators +using only the \samp{!}, \samp{\&}, and \samp{|} operators using the +following rewritings: +\begin{align*} + f\IMPLIES g &\equiv (\NOT f)\OR g\\ + f\EQUIV g &\equiv (f\AND g)\OR ((\NOT g)\AND(\NOT f))\\ + f\XOR g &\equiv (f\AND\NOT g)\OR (g\AND\NOT f)\\ +\end{align*} + +\section{Temporal Operators} + +Given two temporal formul\ae{} $f$, and $g$, the following +temporal operators can be used to construct another temporal formula. + +\begin{center} +\begin{tabular}{ccc} + & preferred & \multicolumn{1}{c}{other supported} \\ + operator & syntax & \multicolumn{1}{c}{syntaxes}\\ + \hline + Next & $\X f$ & $\XALT f$ \\ + Eventually & $\F f$ & $\FALT f$ \\ + Always & $\G f$ & $\GALT f$ \\ + (Strong) Until & $f \U g$ \\ + Weak Until & $f \W g$ \\ + (Weak) Release & $f \R g$ & $f \RALT g$ \\ + Strong Release & $f \M g$ \\ +\end{tabular} +\end{center} + +\subsection{Semantics}\label{sec:opltl:sem} + +\begin{align*} + \sigma\vDash \X f &\iff f\vDash \sigma^{1..}\\ + \sigma\vDash \F f &\iff \exists i\in \N,\, \sigma^{i..}\vDash f\\ + \sigma\vDash \G f &\iff \forall i\in \N,\, \sigma^{i..}\vDash f\\ + \sigma\vDash f\U g &\iff \exists j\in\N,\, + \begin{cases} + \forall i0 \land (\exists k\in\N,\, + (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} + \VDash f\STAR{\mvar{0}..\mvar{j-1}}))\\ + \text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\, + (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} + \VDash f\STAR{\mvar{i-1}..\mvar{j-1}}))\\ + \end{cases}\\ + \sigma\VDash f\STAR{\mvar{i}..} & \iff + \begin{cases} + \text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\ + \text{or} & \mvar{i}=0 \land (\exists k\in\N,\, + (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} + \VDash f\STAR{\mvar{0}..}))\\ + \text{or} & \mvar{i}>0 \land (\exists k\in\N,\, + (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} + \VDash f\STAR{\mvar{i-1}..}))\\ + \end{cases}\\ + \sigma\VDash b\EQUAL{\mvar{i}..\mvar{j}} & \iff + \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..\mvar{j}}\CONCAT\mathtt\{\NOT b\,\mathtt\}\STAR{0..}\\ + \sigma\VDash b\EQUAL{\mvar{i}..} & \iff + \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..}\CONCAT\mathtt\{\NOT b\,\mathtt\}\STAR{0..}\\ + \sigma\VDash b\GOTO{\mvar{i}..\mvar{j}} & \iff + \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..\mvar{j}}\\ + \sigma\VDash b\GOTO{\mvar{i}..} & \iff + \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..}\\ +\end{align*} + +Note that the semantics of $\ANDALT$ and $\AND$ coincide if both +operands are Boolean formul\ae. + +\subsection{Syntactic Sugar} + +The syntax on the left is equivalent to the syntax on the right. +These rewritings are performed from left to right when parsing a +formula, and some are performed from right to left when writing it for +output. + +\begin{align*} + f\STARALT &\equiv f\STAR{0..}\\ + f\STAR{} &\equiv f\STAR{0..} & + f\PLUS{} &\equiv f\STAR{1..} & + f\EQUAL{} &\equiv f\EQUAL{0..} & + f\GOTO{} &\equiv f\GOTO{1..1} \\ + f\STAR{..} &\equiv f\STAR{0..} & + && + f\EQUAL{..} &\equiv f\EQUAL{0..} & + f\GOTO{..} &\equiv f\GOTO{1..} \\ + f\STAR{..\mvar{j}} &\equiv f\STAR{0..\mvar{j}} & + && + f\EQUAL{..\mvar{j}} &\equiv f\EQUAL{0..\mvar{j}} & + f\GOTO{..\mvar{j}} &\equiv f\GOTO{1..\mvar{j}} \\ + f\STAR{\mvar{k}} &\equiv f\STAR{\mvar{k}..\mvar{k}} & + && + f\EQUAL{\mvar{k}} &\equiv f\EQUAL{\mvar{k}..\mvar{k}} & + f\GOTO{\mvar{k}} &\equiv f\GOTO{\mvar{k}..\mvar{k}} \\ + \STAR{} &\equiv \1\STAR{0..} & + \PLUS{} &\equiv \1\STAR{1..} \\ + \STAR{\mvar{k}} &\equiv \1\STAR{\mvar{k}..\mvar{k}} & +\end{align*} + +\subsection{Trivial Identities (Occur Automatically)} + +The following identities also hold if $j$ or $l$ are missing (assuming +they are then equal to $\infty$). $f$ can be any regular expression, +while $b$, $b_1$, $b_2$ are assumed to be Boolean formul\ae. + +\begin{align*} + \0\STAR{0..\mvar{j}} &\equiv \eword & + \0\EQUAL{0..\mvar{j}} &\equiv \1\STAR{} & + \0\GOTO{0..\mvar{j}} &\equiv \eword \\ + \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 & + \0\EQUAL{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0& + \0\GOTO{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0\\ + \eword\STAR{\var{i}..\mvar{j}} &\equiv \eword& + \1\EQUAL{0} &\equiv\eword& + \1\GOTO{0} &\equiv\eword\\ + f\STAR{0}&\equiv \eword & + \1\EQUAL{\mvar{i}..\mvar{j}}&\equiv \1\STAR{\mvar{i}..\mvar{j}}& + \1\GOTO{\mvar{i}..\mvar{j}}&\equiv \1\STAR{\mvar{i}..\mvar{j}}\\ + f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}& + b\EQUAL{0..}&\equiv 1\STAR{} & + b\GOTO{0}&\equiv \eword \\ + &\drsh\text{~if~}i(k+1)\le jk+1 & + b\EQUAL{0}&\equiv (\NOT b)\STAR{} \\ +\end{align*} + +\noindent +The following rules are all valid with the two arguments swapped, except the one marked with $\stackrel{\dag}{\equiv}$. +%(Even for the non-commutative operators \samp{$\CONCAT$} and +%\samp{$\FUSION$}.) + +\begin{align*} + f\AND f &\equiv \0& + f\ANDALT f &\equiv f & + f\OR f &\equiv f \\ + \0\AND f &\equiv f & + \0\ANDALT f &\equiv \0 & + \0\OR f &\equiv f & + \0 \FUSION f &\equiv \0 & + \0 \CONCAT f &\equiv \0 \\ + \1\AND f &\equiv \NOT f& + \1\ANDALT f &\equiv f & + \1\OR f &\equiv \1 & + \1 \FUSION f & \equiv f\\ + \eword\AND f &\equiv f & + \eword\ANDALT f &\equiv + \begin{cases} + \eword \mathrlap{\text{~if~} \varepsilon\VDash f} \\ + \0 \mathrlap{\text{~if~} \varepsilon\nVDash f} \\ + \end{cases} & + && + \eword \FUSION f &\equiv \0 & + \eword \CONCAT f &\equiv f\\ + && + b_1 \ANDALT b_2 &\equiv b_1\AND b_2 & + b:f &\stackrel{\dag}{\equiv} b\AND f\\ +\end{align*} + +\section{Rational-LTL Binding Operators} + +The following operators combine a rational expression $r$ with a PSL +formula $f$ to form another PSL formula. + +\begin{center} +\begin{tabular}{ccccc} + & preferred & \multicolumn{2}{c}{other supported} \\ + operation & syntax & \multicolumn{2}{c}{syntaxes}\\ + \hline + (universal) suffix implication + & $\ratgroup{r}\Asuffix{} f$ + & $\ratgroup{r}\AsuffixALT{} f$ + & $\ratgroup{r}\texttt{(}f\texttt{)}$ + \\ + existential suffix implication + & $\ratgroup{r}\Esuffix{} f$ + \\ + closure + & $\ratgroup{r}$ + \\ + negated closure + & $\nratgroup{r}$ + \\ +\end{tabular} +\end{center} + +For technical reasons, the negated closure is actually implemented as +an operator, even if it is syntactically and semantically equal to the +combination of $\NOT$ and $\ratgroup{r}$. + +\subsection{Semantics} + +The following semantics assume that $r$ is a rational expression, +while $f$ is a PSL formula. + +\begin{align*} + \sigma\vDash \ratgroup{r}\Esuffix f &\iff \exists k\ge 0, (\sigma^{0..k}\VDash r)\land(\sigma^{k..}\vDash f)\\ + \sigma\vDash \ratgroup{r}\Asuffix f &\iff \forall k\ge 0, (\sigma^{0..k}\VDash r)\limplies (\sigma^{k..}\vDash f)\\ + \sigma\vDash \ratgroup{r} & \iff (\exists k\ge 0, \sigma^{0..k}\VDash r)\lor(\forall k\ge 0,\,\exists \pi\in(\B^\AP)^\star,\, (\sigma^{0..k}\prec \pi)\land(\pi\VDash r))\\ + \sigma\vDash \nratgroup{r} & \iff (\forall k\ge 0, \sigma^{0..k}\nVDash r)\land(\exists k\ge 0,\,\exists \forall\in(\B^\AP)^\star,\, (\sigma^{0..k}\prec \pi)\limplies(\pi\nVDash r))\\ +\end{align*} + +The $\prec$ symbol should be read as ``\emph{is a prefix of}''. So +the semantic for `$\sigma\vDash \ratgroup{r}$' is that either there is +a finite prefix of $\sigma$ that is a model of $r$, or any prefix of +$\sigma$ can be extended into a finite sequence $\pi$ that is a model +of $r$. An infinite sequence $\texttt{a;a;a;a;a;}\ldots$ is therefore a +model of the formula \samp{$\ratgroup{a\PLUS{};\NOT a}$} even though +it never sees \samp{$\NOT a$}. + +\subsection{Syntactic Sugar} + +The syntax on the left is equivalent to the syntax on the right. +These rewritings are performed from left to right when parsing a +formula.\spottodo{It would be nice to have the opposite rewritings on + output.} + +\begin{align*} + \ratgroup{r}\EsuffixEQ f &\equiv \ratgroup{r\CONCAT\1}\Esuffix f & + \ratgroup{r}\AsuffixEQ f &\equiv \ratgroup{r\CONCAT\1}\Asuffix f\\ + \ratgroupn{r} &\equiv \ratgroup{r}\Esuffix \1 & + \ratgroup{r}\AsuffixALTEQ f &\equiv \ratgroup{r\CONCAT\1}\Asuffix f\\ +\end{align*} + +$\AsuffixEQ$ and $\AsuffixALTEQ$ are synonyms in the same way as +$\Asuffix$ and $\AsuffixALT$ are. + +\subsection{Trivial Identities (Occur Automatically)} + +For any PSL formula $f$, any rational expression $r$, and any Boolean +formula $b$, the following rewritings are systematically performed +(from left to right). + +\begin{align*} + \ratgroup{\0}\Asuffix f &\equiv \1 +& \ratgroup{\0}\Esuffix f &\equiv \0 +& \ratgroup{\0} & \equiv \0 +& \nratgroup{\0} & \equiv \1 \\ + \ratgroup{\1}\Asuffix f &\equiv f +& \ratgroup{\1}\Esuffix f &\equiv f +& \ratgroup{\1} & \equiv \1 +& \nratgroup{\1} & \equiv \0 \\ + \ratgroup{\eword}\Asuffix f&\equiv \1 +& \ratgroup{\eword}\Esuffix f&\equiv \0 +& \ratgroup{\eword} & \equiv \0 +& \nratgroup{\eword} & \equiv \1 \\ + \ratgroup{r}\Asuffix \1&\equiv \1 +& \ratgroup{r}\Esuffix \0&\equiv \0 \\ + \ratgroup{b}\Asuffix f&\equiv b\IMPLIES f +& \ratgroup{b}\Esuffix f&\equiv b\AND f \\ +\end{align*} + +\chapter{Grammar} + +For simplicity, this grammar gives only one rule for each +operator, even if the operator has multiple synonyms (like \samp{|}, +\samp{||}, and {`\verb=\/='}). + +\begin{align*} + \mathit{constant} ::=&\, \0 \mid \1 & \mathit{tformula} ::=&\,\mathit{bformula}\\ + \mathit{atomic\_prop} ::=&\, \text{see section~\ref{sec:ap}} & \mid&\,\tsamp{(}\,\mathit{tformula}\,\tsamp{)} \\ + \mathit{bformula} ::=&\, \mathit{constant} & \mid&\,\msamp{\NOT}\,\mathit{tformula}\,\\ + \mid&\,\mathit{atomic\_prop} & \mid&\,\mathit{tformula}\,\msamp{\AND}\,\mathit{tformula} \\ + \mid&\,\tsamp{(}\,\mathit{bformula}\,\tsamp{)} & \mid&\,\mathit{tformula}\,\msamp{\OR}\,\mathit{tformula} \\ + \mid&\,\msamp{\NOT}\,\mathit{bformula} & \mid&\,\mathit{tformula}\,\msamp{\IMPLIES}\,\mathit{tformula} \\ + \mid&\,\mathit{bformula}\,\msamp{\AND}\,\mathit{bformula} & \mid&\,\mathit{tformula}\,\msamp{\XOR}\,\mathit{tformula} \\ + \mid&\,\mathit{bformula}\,\msamp{\OR}\,\mathit{bformula} & \mid&\,\mathit{tformula}\,\msamp{\EQUIV}\,\mathit{tformula} \\ + \mid&\,\mathit{bformula}\,\msamp{\IMPLIES}\,\mathit{bformula} & \mid&\,\msamp{\X}\,\mathit{tformula}\\ + \mid&\,\mathit{bformula}\,\msamp{\XOR}\,\mathit{bformula} & \mid&\,\msamp{\F}\,\mathit{tformula}\\ + \mid&\,\mathit{bformula}\,\msamp{\EQUIV}\,\mathit{bformula} & \mid&\,\msamp{\G}\,\mathit{tformula}\\ + \mathit{rformula} ::=&\, \mathit{bformula} & \mid&\,\mathit{tformula}\,\msamp{\U}\,\mathit{tformula} \\ + \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}} & \mid&\,\mathit{tformula}\,\msamp{\W}\,\mathit{tformula} \\ + \mid&\,\mathit{rformula}\msamp{\OR}\mathit{rformula} & \mid&\,\mathit{tformula}\,\msamp{\R}\,\mathit{tformula} \\ + \mid&\,\mathit{rformula}\msamp{\AND}\mathit{rformula} & \mid&\,\mathit{tformula}\,\msamp{\M}\,\mathit{tformula} \\ + \mid&\,\mathit{rformula}\msamp{\ANDALT}\mathit{rformula} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\Asuffix}\,\mathit{tformula}\\ + \mid&\,\mathit{rformula}\msamp{\CONCAT}\mathit{rformula} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\AsuffixEQ}\,\mathit{tformula}\\ + \mid&\,\mathit{rformula}\msamp{\FUSION}\mathit{rformula} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\Esuffix}\,\mathit{tformula}\\ + \mid&\,\mathit{rformula}\msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\EsuffixEQ}\,\mathit{tformula} \\ + \mid&\,\mathit{rformula}\msamp{\PLUS} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}} \\ + \mid&\,\mathit{rformula}\msamp{\EQUAL{\mvar{i}..\mvar{j}}} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\msamp{\NOT} \\ + \mid&\,\mathit{rformula}\msamp{\GOTO{\mvar{i}..\mvar{j}}} \\ +\end{align*} + +\section{Operator precedence} + +\ltltodo[inline]{Document operator precedence.} + +\chapter{Properties} + +When Spot builds a formula (represented by an AST with shared +subtrees) it computes a set of properties for each node. These +properties can be queried from any \texttt{spot::ltl::formula} +instance using the following methods: + +\noindent +\begin{tabulary}{\textwidth}{lL} +\texttt{is\_boolean()}& Whether the formula use only Boolean + operators. +\\\texttt{is\_sugar\_free\_boolean()}& Whether the formula use + only $\AND$, $\OR$, and $\NOT$ operators. (Especially, no + $\IMPLIES$ or $\EQUIV$ are allowed.) +\\\texttt{is\_in\_nenoform()}& Whether the formula is in negative + normal form. See section~\ref{sec:nnf}. +\\\texttt{is\_X\_free()}& + Whether the formula avoids the $\X$ operator. +\\\texttt{is\_ltl\_formula()}& Whether the formula uses only LTL + operators. (Boolean operators are also allowed.) +\\\texttt{is\_eltl\_formula()}& Whether the formula uses only ELTL + operators. (Boolean and LTL operators are also allowed.) +\\\texttt{is\_psl\_formula()}& Whether the formula uses only PSL + operators. (Boolean and LTL operators are also allowed.) +\\\texttt{is\_sere\_formula()}& Whether the formula uses only + rational operators. (Boolean operators are also allowed, provided + no rational operator is negated.) +\\\texttt{is\_finite()}& Whether a SERE describes a finite + language, or an LTL formula uses no temporal operator but $\X$. +\\\texttt{is\_eventual()}& Whether the formula is a pure eventuality. +\\\texttt{is\_universal()}& Whether the formula is purely universal. +\\\texttt{is\_syntactic\_safety()}& Whether the formula is a syntactic + safety property. +\\\texttt{is\_syntactic\_guaranty()}& Whether the formula is a syntactic + guaranty property. +\\\texttt{is\_syntactic\_obligation()}& Whether the formula is a syntactic + obligation property. +\\\texttt{is\_syntactic\_recurrence()}& Whether the formula is a syntactic + recurrence property. +\\\texttt{is\_syntactic\_persistence()}& Whether the formula is a syntactic + persistence property. +\\\texttt{is\_marked()}& Whether the formula contains a special + ``marked'' version of the $\Esuffix$ operator.\footnote{This special + operator is used when translating recurring $\Esuffix$, it is + rendered as $\EsuffixMarked$ and it obeys the same simplification + rules and properties as $\Esuffix$ (except for the + \texttt{is\_marked()} property).} +\\\texttt{accepts\_eword()}& Whether the formula accept + $\eword$. (This can only be true for a rational formula.) +\end{tabulary} + +\section{Pure Eventualities and Purely Universal Formul\ae{}} +\label{sec:eventuniv} + +These two syntactic classes of formul\ae{} were introduced +by~\citet{etessami.00.concur} to simplify LTL formul\ae{}. We shall +present the associated simplification rules in +Section~\ref{sec:eventunivrew}, for now we only define these two +classes. + +Pure eventual formul\ae{} describe properties that are left-append +closed, i.e., any accepted (infinite) sequence can be prefixed by a +finite sequence and remain accepted. From an LTL standpoint, if +$\varphi$ is a left-append closed formula, then $\F\varphi \equiv +\varphi$. + +Purely universal formul\ae{} describe properties that are +suffix-closed, i.e., if you remove any finite prefix of an accepted +(infinite) sequence, it remains accepted. From an LTL standpoint if +$\varphi$ is a suffix-closed formula, then $\G\varphi \equiv \varphi$. + + +Let $\varphi$ designate any arbitrary formula and $\varphi_E$ +(resp. $\varphi_U$) designate any instance of a pure eventuality +(resp. a purely universal) formula. We have the following grammar +rules: + +\begin{align*} + \varphi_E ::=&\, \0 + \mid \1 + \mid \X \varphi_E + \mid \F \varphi + \mid \G \varphi_E + \mid \varphi_E\AND \varphi_E + \mid (\varphi_E\OR \varphi_E) + \mid \NOT\varphi_U\\ + \mid&\,\varphi \U \varphi_E + \mid 1 \U \varphi + \mid \varphi_E\R \varphi_E + \mid \varphi_E\W \varphi_E + \mid \varphi_E\M \varphi_E + \mid \varphi \M \1\\ + \varphi_U ::=&\, \0 + \mid \1 + \mid \X \varphi_U + \mid \F \varphi_U + \mid \G \varphi + \mid \varphi_U\AND \varphi_U + \mid (\varphi_U\OR \varphi_U) + \mid \NOT\varphi_E\\ + \mid&\,\varphi_U\U \varphi_U + \mid \varphi \R \varphi_U + \mid \0 \R \varphi + \mid \varphi_U\W \varphi_U + \mid \varphi \W \0 + \mid \varphi_U\M \varphi_U\\ +\end{align*} + +\section{Syntactic Hierarchy Classes} + +The hierarchy of linear temporal properties was introduced +by~\citet{manna.87.podc}. A first syntactic characterization of the +classes was presented by~\citet{chang.92.icalp}, but other +presentations have been done including negation~\citep{cerna.03.mfcs} +and weak until~\citep{schneider.01.lpar}. + +In the following grammar rules, the symbols $\varphi_G$, $\varphi_S$, +$\varphi_O$, $\varphi_P$, $\varphi_R$ designate any formula belonging +respectively to the Guarantee, Safety, Obligation, Persistence, or +Recurrence classes. $v$ designates any variable, $r$ any rational +property, $r_F$ a finite rational property (no loops), and $r_I$ an +infinite rational property. + + +\begin{align*} + \varphi_G ::=&\, \0\mid\1\mid v\mid \NOT\varphi_S\mid + \varphi_G\AND \varphi_G\mid (\varphi_G\OR \varphi_G)\mid + \X\varphi_G \mid \F\varphi_G\mid + \varphi_G\U\varphi_G\mid \varphi_G\M\varphi_G\\ + \mid&\, \ratgroup{r}\Esuffix \varphi_G\mid + \ratgroup{r_F}\Asuffix \varphi_G\\ + \varphi_S ::=&\, \0\mid\1\mid v\mid \NOT\varphi_G\mid + \varphi_S\AND \varphi_S\mid (\varphi_S\OR \varphi_S)\mid + \X\varphi_S \mid \G\varphi_S\mid + \varphi_S\R\varphi_S\mid \varphi_S\W\varphi_S\\ + \mid&\, \ratgroup{r_F}\Esuffix \varphi_S\mid + \ratgroup{r}\Asuffix \varphi_S\\ + \varphi_O ::=&\, \varphi_G \mid \varphi_S\mid \NOT\varphi_O\mid + \varphi_O\AND \varphi_O\mid (\varphi_O\OR \varphi_O)\mid + \X\varphi_O \mid + \varphi_O\U\varphi_G\mid\varphi_O\R\varphi_S \mid + \varphi_S\W\varphi_O\mid \varphi_G\M\varphi_O\\ + \mid&\, \ratgroup{r_F}\Esuffix \varphi_O \mid \ratgroup{r_I}\Esuffix \varphi_G\mid + \ratgroup{r_F}\Asuffix \varphi_O\mid + \ratgroup{r_I}\Asuffix \varphi_S\\ + \varphi_P ::=&\, \varphi_O \mid \NOT\varphi_R\mid + \varphi_P\AND \varphi_P\mid (\varphi_P\OR \varphi_P)\mid + \X\varphi_P \mid \F\varphi_P \mid + \varphi_P\U\varphi_P\mid\varphi_P\R\varphi_S\mid + \varphi_S\W\varphi_P\mid\varphi_P\M\varphi_P\\ + \mid&\, \ratgroup{r}\Esuffix \varphi_P\mid + \ratgroup{r_F}\Asuffix \varphi_P\mid + \ratgroup{r_I}\Asuffix \varphi_S\\ + \varphi_R ::=&\, \varphi_O \mid \NOT\varphi_P\mid + \varphi_R\AND \varphi_R\mid (\varphi_R\OR \varphi_R)\mid + \X\varphi_R \mid \G\varphi_R \mid + \varphi_R\U\varphi_G\mid\varphi_R\R\varphi_R\mid + \varphi_R\W\varphi_R\mid\varphi_G\M\varphi_R\\ + \mid&\, \ratgroup{r_F}\Esuffix \varphi_R \mid \ratgroup{r_I}\Esuffix \varphi_G\mid \ratgroup{r}\Asuffix \varphi_P\\ +\end{align*} + +\chapter{Rewritings} + +The LTL rewritings described in this section are all implemented in +the `\verb|ltl_simplifier|' class defined in +\texttt{spot/ltlvisit/simplify.hh}. This class implements several +caches in order to quickly rewrite formul\ae{} that have already been +rewritten previously. For this reason, it is suggested that you reuse +your instance of `\verb|ltl_simplifier|' as much as possible. If you +write an algorithm that will simplify LTL formul\ae{}, we suggest you +accept an optional `\verb|ltl_simplifier|' argument, so that you can +benefit from an existing instance. + +The `\verb|ltl_simplifier|' takes an optional +`\verb|ltl_simplifier_options|' argument, making it possible to tune +the various rewritings that can be performed by this class. These +options cannot be changed afterwards (because changing these options +would invalidate the results stored in the caches). + +\section{Negative normal form}\label{sec:nnf} + +This is implemented by the `\verb|ltl_simplifier::negative_normal_form|` +method. + +A formula in negative normal form can only have only have negation +operators ($\NOT$) in front of atomic properties, and does not use any +of the $\XOR$, $\IMPLIES$ and $\EQUIV$ operators. The following +rewriting arrange any PSL formula into negative normal form. + +\begin{align*} + \NOT\X f & \equiv \X\NOT f & + \NOT(f \U g) & \equiv (\NOT f) \R (\NOT g) & + \NOT(f \AND g)&\equiv (\NOT f) \OR (\NOT g) + \\ + \NOT\F f & \equiv \G\NOT f & + \NOT(f \R g) & \equiv (\NOT f) \U (\NOT g) & + \NOT(f \OR g)&\equiv (\NOT f)\AND (\NOT g) + \\ + \NOT\G f & \equiv \F\NOT f & + \NOT(f \W g) & \equiv (\NOT f) \M (\NOT g) & + \NOT(\ratgroup{r} \Asuffix f) &\equiv \ratgroup{r} \Esuffix \NOT f + \\ + \NOT(\ratgroup{r})&\nratgroup{r}& + \NOT(f \M g) & \equiv (\NOT f) \W (\NOT g)& + \NOT(\ratgroup{r} \Esuffix f) &\equiv \ratgroup{r} \Asuffix \NOT f +\end{align*} +\noindent Recall the that negated closure $\nratgroup{r}$ is actually +implemented as a specific operator, so it not actually prefixed by the +$\NOT$ operator. +\begin{align*} + f \XOR g & \equiv ((\NOT f)\AND g)\OR(f\AND\NOT g) & + \NOT(f \XOR g) & \equiv ((\NOT f)\AND(\NOT g))\OR(f\AND g) & + \NOT(f \AND g) & \equiv (\NOT f)\OR(\NOT g) \\ + f \EQUIV g & \equiv ((\NOT f)\AND(\NOT g))\OR(f\AND g) & + \NOT(f \EQUIV g) & \equiv ((\NOT f)\AND g)\OR(f\AND\NOT g) & + \NOT(f \OR g) & \equiv (\NOT f)\AND(\NOT g) \\ + f \IMPLIES g & \equiv (\NOT f) \AND g & + \NOT(f \IMPLIES g) & \equiv f \AND \NOT g +\end{align*} + +Note that the above rules include those from +`\verb=unabbreviate_logic_visitor=` described in +Section~\ref{sec:unabbbool}. Therefore it is never necessary to apply +`\verb=unabbreviate_logic_visitor=` before or after +`\verb|ltl_simplifier::negative_normal_form|`. + +If the option `\verb|nenoform_stop_on_boolean|' is set, the above +recursive rewriting will not be applied to subformul\ae{} that are +Boolean formul\ae. For instance calling +`\verb|ltl_simplifier::negative_normal_form|` on $\NOT\F\G(a \XOR b)$ +will produce $\G\F(((\NOT a)\AND(\NOT b))\OR(a\AND b))$ if +`\verb|nenoform_stop_on_boolean|' is unset, while it will produce +$\G\F(\NOT(a \XOR b))$ if `\verb|nenoform_stop_on_boolean|' is set. + +\section{Simplifications} + +The `\verb|ltl_simplifier::simplify|' method performs several kinds of +simplifications, depending on which `\verb|ltl_simplifier_options|' +was set. + +The goals in most of these simplification are to: +\begin{itemize} +\item remove useless terms and operator. +\item move the $\X$ operators to the front of the formula (e.g., $\X\G + f$ is better than the equivalent $\G\X f$). This is because LTL + translators will usually want to rewrite LTL formul\ae{} in + a kind of disjunctive form: $\displaystyle\bigvee_i + \left(\beta_i\land\X\psi_i\right)$ where $\beta_i$s are Boolean + formul\ae{} and $\psi_i$s are LTL formul\ae{}. Moving $\X$ to the + front therefore simplify the translation. +\item move the $\F$ operators to the front of the formula (e.g., $\F(f + \OR g)$ is better than the equivalent $(\F f)\OR (\F g)$), but not + before $\X$ ($\X\F f$ is better than $\F\X f$). Because $\F f$ + incurs some indeterminism, it is best to factorize these terms to + limit the sources of indeterminism. +\end{itemize} + +\subsection{Basic Simplifications} + +These simplifications are enabled with +\verb|ltl_simplifier_options::reduce_basics|'. + + +The following are simplification rules for unary operators (applied +from left to right, as usual): +\begin{align*} + \X\F\G f &\equiv \F\G f & \X\G\F f &\equiv \G\F f \\ + \F(f\U g) &\equiv \F g & \F\X f &\equiv \X\F f \\ + \G(f \R g) &\equiv \G g & \G\X f &\equiv \X\G f +\end{align*} +\begin{align*} + \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m))&\equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m) +\end{align*} +Note that the latter three rewriting rules for $\G$ have no dual: +rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (instance as +suggested by~\citet{somenzi.00.cav}) goes against our goal of moving +the $\F$ operator in front of the formula. Conceptually, it is also +easier to understand $\F(f \AND \G\F g)$: has long as $f$ has not been +verified, there is no need to worry about the $\G\F g$ term. + +Here are the basic rewriting rules for binary operators (excluding $\OR$ and +$\AND$ which are considered in Spot as $n$-ary operators): +\begin{align*} + \1 \U f &\equiv \F f & f \W \0 &\equiv \G f \\ + f \M \1 &\equiv \F f & \0 \R f &\equiv \G f \\ + (\X f)\U (\X g) &\equiv \X(f\U g) & (\X f)\W(\X g) &\equiv \X(f\W g) \\ + (\X f)\M (\X g) &\equiv \X(f\M g) & (\X f)\R(\X g) &\equiv \X(f\R g) \\ + f \U(\G f) &\equiv \G f & f \W(\G f) &\equiv \G f \\ + f \M(\F f) &\equiv \F f & f \R(\F f) &\equiv \F f \\ + f \U (g \OR \G(f)) &\equiv f\W g & f \W (g \OR \G(f)) &\equiv f\W g\\ + f \M (g \AND \F(f)) &\equiv f\M g & f \R (g \AND \F(f)) &\equiv f\M g +\end{align*} + +Here are the basic rewriting rules for $n$-ary operators ($\AND$ and +$\OR$): +\begin{align*} + (\F\G f) \AND(\F\G g) &\equiv \F\G(f\AND g) & + (\G\F f) \OR (\G\F g) &\equiv \G\F(f\OR g) \\ + (\X f) \AND(\X g) &\equiv \X(f\AND g) & + (\X f) \OR (\X g) &\equiv \X(f\OR g) \\ + (\X f) \AND(\F\G g) &\equiv \X(f\AND \F\G g) & + (\X f) \OR (\G\F g) &\equiv \X(f\OR \G\F g) \\ + (f_1 \U f_2)\AND (f_3 \U f_2)&\equiv (f_1\AND f_3)\U f_2& + (f_1 \U f_2)\OR (f_1 \U f_3)&\equiv f_1\U (f_2\OR f_3) \\ + (f_1 \U f_2)\AND (f_3 \W f_2)&\equiv (f_1\AND f_3)\U f_2& + (f_1 \U f_2)\OR (f_1 \W f_3)&\equiv f_1\W (f_2\OR f_3) \\ + (f_1 \W f_2)\AND (f_3 \W f_2)&\equiv (f_1\AND f_3)\W f_2& + (f_1 \W f_2)\OR (f_1 \W f_3)&\equiv f_1\W (f_2\OR f_3) \\ + (f_1 \R f_2)\AND (f_1 \R f_3)&\equiv f_1\R (f_2\AND f_3)& + (f_1 \R f_2)\OR (f_3 \R f_2)&\equiv (f_1\OR f_3) \R f_2\\ + (f_1 \R f_2)\AND (f_1 \M f_3)&\equiv f_1\M (f_2\AND f_3)& + (f_1 \R f_2)\OR (f_3 \M f_2)&\equiv (f_1\OR f_3) \R f_3\\ + (f_1 \M f_2)\AND (f_1 \M f_3)&\equiv f_1\M (f_2\AND f_3)& + (f_1 \M f_2)\OR (f_3 \M f_2)&\equiv (f_1\OR f_3) \M f_3\\ + (\F g)\AND (f \U g)&\equiv f\U g & + (\G f)\OR (f \U g)&\equiv f\W g \\ + (\F g)\AND (f \W g)&\equiv f\U g & + (\G f)\OR (f \W g)&\equiv f\W g \\ + (\F f)\AND (f \R g)&\equiv f\M g & + (\G g)\OR (f \R g)&\equiv f\R g \\ + (\F f)\AND (f \M g)&\equiv f\M g & + (\G g)\OR (f \M g)&\equiv f\R g +\end{align*} +The above rules are applied even if more terms are presents in the +operator's arguments. For instance $\F\G(a)\AND \G(b) \AND \F\G(c) \AND +\X(d)$ will be rewritten as $\X(d \AND \F\G(a\AND c))\AND \G(b)$. + +Finally the following rule is applied only when no other terms are present +in the OR arguments: +\begin{align*} + \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m) + &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots \OR g_m)) \\ +\end{align*} + +\subsection{Simplifications for Eventual and Universal Formul\ae} +\label{sec:eventunivrew} + +The class of \textit{pure eventuality} and \textit{purely universal} +formul\ae{} are described in section~\ref{sec:eventuniv}. + +In the following rewritings, we use the following +notation to distinguish the class of subformul\ae: + +\begin{center} +\begin{tabular}{rl} +\hline +$f,\,f_i,\,g,\,g_i$ & any PSL formula \\ +$e,\,e_i$ & a pure eventuality \\ +$u,\,u_i$ & a purely universal formula \\ +$q,\,q_i$ & a pure eventuality that is also purely universal \\ +\hline +\end{tabular} +\end{center} + +\begin{align*} + \F e &\equiv e & f \U e &\equiv e & e \M f &\equiv e\AND f \\ + \G u &\equiv u & f \R u &\equiv u & u \W f &\equiv u\OR f \\ + \X q &\equiv q & q \AND \X f &\equiv \X(q \AND f) & q\OR \X f &\equiv \X(q \OR f) +\end{align*} +\begin{align*} + \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)\OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)\OR q_1 \OR \ldots q_p \\ +\intertext{Finally the following rule is applied only when no other + terms are present in the OR arguments:} + \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m) + \OR q_1 \OR \ldots \OR q_p + &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots\OR g_m) \OR q_1\OR \ldots q_p) +\end{align*} + +\subsection{Simplifications Based on Implications} +\label{sec:syntimpl} + +The following rewriting rules are performed only when we can prove +that some subformula $f$ implies another subformula $g$. Showing such +implication can be done in two ways: +\begin{description} +\item[Syntactic Implication Checks] were initially proposed + by~\citet{somenzi.00.cav}. This detection is enabled by the + ``\verb|ltl_simplifier_options::synt_impl|'' option. This is a + cheap way to detect implications, but it may miss some. The rules + we implement are described in Annex~\ref{ann:syntimpl}. + +\item[Language Containment Checks] were initially proposed + by~\citet{tauriainen.03.a83}. This detection is enabled by the + ``\verb|ltl_simplifier_options::containment_checks|'' option. +\end{description} + +In the following rewritings rules, $f\simp g$ means that $g$ was +proved to be implied by $f$ using either of the above two methods. +Additionally, implications denoted by $f\Simp g$ are only checked +if the ``\verb|ltl_simplifier_options::containment_checks_stronger|'' +option is set (otherwise the rewriting rule is not applied). + +\begin{equation*} +\begin{array}{cccr@{\,}l} +\text{if}& f\simp g &\text{then}& f\OR g &\equiv g \\ +\text{if}& f\simp g &\text{then}& f\AND g &\equiv f \\ +\text{if}& f\simp \NOT g &\text{then}& f\OR g &\equiv \1 \\ +\text{if}& f\simp \NOT g &\text{then}& f\AND g &\equiv \0 \\ +\text{if}& f\simp g &\text{then}& f\U g &\equiv g \\ +\text{if}& (f\U g)\Simp g &\text{then}& f\U g &\equiv g \\ +\text{if}& (\NOT f)\simp g &\text{then}& f\U g &\equiv \F g \\ +\text{if}& f\simp g &\text{then}& f\U (g \U h) &\equiv g \U h \\ +\text{if}& f\simp g &\text{then}& f\U (g \W h) &\equiv g \W h \\ +\text{if}& f\simp g &\text{then}& f\W g &\equiv g \\ +\text{if}& (f\W g)\Simp g &\text{then}& f\W g &\equiv g \\ +\text{if}& (\NOT f)\simp g &\text{then}& f\W g &\equiv \1 \\ +\text{if}& f\simp g &\text{then}& f\W (g \W h) &\equiv g \W h \\ +\text{if}& g\simp f &\text{then}& f\R g &\equiv g \\ +\text{if}& g\simp \NOT f &\text{then}& f\R g &\equiv \G g \\ +\text{if}& g\simp f &\text{then}& f\R (g \R h) &\equiv g \R h \\ +\text{if}& g\simp f &\text{then}& f\R (g \M h) &\equiv g \M h \\ +\text{if}& f\simp g &\text{then}& f\R (g \R h) &\equiv f \R h \\ +\text{if}& g\simp f &\text{then}& f\M g &\equiv g \\ +\text{if}& g\simp \NOT f &\text{then}& f\M g &\equiv \0 \\ +\text{if}& g\simp f &\text{then}& f\M (g \M h) &\equiv g \M h \\ +\text{if}& f\simp g &\text{then}& f\M (g \M h) &\equiv f \M h \\ +\text{if}& f\simp g &\text{then}& f\M (g \R h) &\equiv f \M h \\ +\end{array} +\end{equation*} + + +\appendix +\chapter{Syntactic Implications}\label{ann:syntimpl} + +Syntactic implications are used for the rewriting of +Section~\ref{sec:syntimpl}. The rules presented bellow extend those +first presented by~\citet{somenzi.00.cav}. + +A few words about implication first. For two PSL formul\ae{} $f$ and +$g$, we say that $f\implies g$ if $\forall\sigma,\,(\sigma\vDash +f)\implies(\sigma\vDash g)$. For two rational formul\ae{} $f$ and +$g$, we say that $f\implies g$ if $\forall\pi,\,(\pi\VDash +f)\implies(\pi\VDash g)$. + +The recursive rules for syntactic implication are rules are described +in table~\ref{tab:syntimpl}, in which $\simp$ denotes the syntactic +implication, $f$, $f_1$, $f_2$, $g$, $g_1$ and $g_2$ designate any PSL +formula in negative normal form, and $f_U$ and $g_E$ designate a +purely universal formula and a pure eventuality. + +The form on the left of the table syntactically implies the form on +the top of the table if the condition in the corresponding cell holds. + +Note that a given formula may match several forms, and require +multiple recursive tests. To limit the number of recursive calls, +some rules have been removed when they are already implied by other +rules. + +For instance it one would legitimately expect the rule ``$\F f \simp +\F g$ \textit{if} $f\simp g$'' to appear in the table. However in +that case $\F g$ is pure eventuality, so we can reach the same +conclusion by chaining two rules: ``$\F f \simp \underbrace{\F + g}_{g_E}$ \textit{if} $f\simp \underbrace{\F g}_{g_E}$'' and then +``$f \simp \F g$ \textit{if} $f\simp g$''. + +The rules from table~\ref{tab:syntimpl} should be completed by the +following cases, where $f_b$ and $g_b$ designate Boolean formul\ae{}: +\begin{center} +\begin{tabular}{rl} +we have & if \\ +\hline +$f\simp \1$ & always \\ +$\0\simp g$ & always \\ +$f_b \simp g_b$ & $\mathrm{BDD}(f_b)\land \mathrm{BDD}(g_b) = + \mathrm{BDD}(f_b)$ \\ +\end{tabular} +\end{center} + +\begin{sidewaystable} +\footnotesize +\def\bone#1#2{$\phantom{{}\land{}} #1\simp #2$} +\def\bor#1#2#3#4{$\begin{aligned}#1 &\simp #2 \\{}\lor #3 &\simp #4\end{aligned}$} +\def\band#1#2#3#4{$\begin{aligned}#1 &\simp #2 \\{}\land #3 &\simp #4\end{aligned}$} +\def\banD#1#2#3#4#5#6{$\begin{aligned}#1 &\simp #2 \\{}\land #3 &\simp #4\\{}\land #5 &\simp #6\end{aligned}$} + +\begin{center} +\begin{tabular}{|c||c|c|c|c|c|c|c|c|c|c|c|} +\hline +$\simp$ & $g$ & $g_E$ & $\X g$ & $g_1\U g_2$ & $g_1\W g_2$ & $g_1 \R g_2$ & $g_1\M g_2$ & $\F g$ & $\G g$ & $g_1\OR g_2$ & $g_1 \AND g_2$ \\ +\hline +\hline +$f$ & $f=g$ & & & \bone{f}{g_2} & \bone{f}{g_2} & \band{f}{g_1}{f}{g_2} & \band{f}{g_1}{f}{g_2} & \bone{f}{g} & & \bor{f}{g_1}{f}{g_2} & \band{f}{g_1}{f}{g_2} \\ +\hline +$f_U$ & & & $f_U\simp g$ & & & & & & $f_U \simp g$ & & \\ +\hline +$\X f$ & & $f\simp g_E$ & $f\simp g$ & & & & & & & & \\ +\hline +$f_1\U f_2$ & \band{f_1}{g}{f_2}{g} & & & \band{f_1}{g_1}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} & \bone{f_2}{g} & & & \\ +\hline +$f_1\W f_2$ & \band{f_1}{g}{f_2}{g} & & & \band{f_1}{g_2}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} & & \band{f_1}{g}{f_2}{g} & & & \\ +\hline +$f_1\R f_2$ & \bone{f_2}{g} & & & & \band{f_1}{g_2}{f_2}{g_1} & \band{f_1}{g_1}{f_2}{g_2} & \band{f_2}{g_1}{f_2}{g_2} & \bone{f_2}{g} & & & \\ +\hline +$f_1\M f_2$ & \bone{f_2}{g} & & & \band{f_1}{g_2}{f_2}{g_1} & \band{f_1}{g_2}{f_2}{g_1} & \band{f_1}{g_1}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \bor{f_1}{g}{f_2}{g} & & & \\ +\hline +$\F f$ & & $f\simp g_E$ & & & & & & & & & \\ +\hline +$\G f$ & \bone{f}{g} & & & \bone{f}{g_2} & \bor{f}{g_1}{f}{g_2} & \bone{f}{g_2} & \band{f}{g_1}{f}{g_2} & & & & \\ +\hline +$f_1\OR f_2$ & \band{f_1}{g}{f_2}{g} & & & & & & & & & & \\ +\hline +$f_1\AND f_2$ & \bor{f_1}{g}{f_2}{g} & & & & & & & & & & \\ +\hline +\end{tabular} +\end{center} +\caption{Recursive rules for syntactic implication.\label{tab:syntimpl}} +\end{sidewaystable} + + +\phantomsection % fix hyperlinks +\addcontentsline{toc}{chapter}{\bibname} +\bibliographystyle{plainnat} +\bibliography{tl} + +\end{document} +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: