Add PTG things to manual

imitator-model-checker · Nov 12, 2023 · 76f61ac · 76f61ac
1 parent 9e7bdf0
commit 76f61ac
Show file tree

Hide file tree

Showing 2 changed files with 70 additions and 2 deletions.
diff --git a/doc/IMITATOR-user-manual.tex b/doc/IMITATOR-user-manual.tex
@@ -2667,6 +2667,17 @@ \section{Parametric non-Zeno cycle synthesis}\label{section:algorithm:Zeno}
 	The \emph{accepting} cycles are not (yet?)\ supported for non-Zeno synthesis.
 \end{remark}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Parametric Timed Game parameter synthesis}\label{section:algorithm:ptg}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+Given a Parametric Timed Game (PTA enriched with controllable/uncontrollable actions) synthesizes a parameter constraint such that, for any parameter valuation in that constraint, a winning strategy exists for the controllable player. Based on the algorithm on Timed Games described in~\cite{DBLP:conf/concur/CassezDFLL05} and further extended for Parametric Timed Games in \cite{DBLP:conf/wodes/JovanovicFLR12}.
+
+The property syntax is of the following form:
+
+\begin{IMITATORproperty}
+property := #synth Win(state_predicate);
+\end{IMITATORproperty}
+
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -2895,6 +2906,10 @@ \section{Summary}\label{section:algorithm:summary}
 			\hline
 			PRPC                   & \styleIMI{PRPC(state\_pred, hyper\_rect)}        & \cellYes{} & \cellNo{} & \cellNo{} \\
 
+			% PTG
+			\hline
+			PTG                   & \styleIMI{Win(state\_pred)}        & \cellYes{} & \cellYes{} & \cellNo{} \\
+
 			% Observer patterns
 
 			\hline
@@ -2990,6 +3005,11 @@ \section{Summary}\label{section:algorithm:summary}
 			\hline
 			PRPC                   & \styleIMI{PRPC(state\_pred, hyper\_rect)}        & \cellYes{} & \styleOption{inclusion}  \\
 
+			% PTG
+
+			\hline
+			PTG                   & \styleIMI{Win(state\_pred)}        & \cellNo{} & \styleOption{inclusion}  \\
+
 			% Observer patterns = reachability
 
 			\hline
@@ -4444,8 +4464,8 @@ \subsection{Automata descriptions}
 \regleGrammaire{controllable\_actions}
 %------------------------------------------------------------
 \begin{longtable}{p{1em} p{.88\textwidth}}
-
 	$|$ & \styleIMI{controllable actions:} \nt{name\_list} \styleIMI{;} \\
+	$|$ & \styleIMI{uncontrollable actions:} \nt{name\_list} \styleIMI{;} \\
 	$|$ & \emptystring
 \end{longtable}
 
@@ -5489,8 +5509,11 @@ \section{Grammar of the property file}\label{section:grammar-property}
 	$|$ & \styleIMI{BCrandomseq} \styleIMI{(} \nt{hyper\_rectangle} \styleIMI{,} \nt{pos\_integer} \nt{step\_opt} \styleIMI{)} \\
 	$|$ & \styleIMI{PRPC} \styleIMI{(} \nt{state\_predicate} \styleIMI{,} \nt{hyper\_rectangle} \nt{step\_opt} \styleIMI{)}    \\
 
+	% PTG
+	$|$ & \styleIMI{Win(} \nt{state\_predicate} \styleIMI{)}    																\\ 
+
 	% Observer pattern
-	$|$ & \styleIMI{pattern(} \nt{pattern} \styleIMI{)}                                                                                                       \\
+	$|$ & \styleIMI{pattern(} \nt{pattern} \styleIMI{)}                                                                                                 \\
 \end{longtable}
 
 

diff --git a/doc/biblio.bib b/doc/biblio.bib
@@ -1070,3 +1070,48 @@ @article{WSWLSDYL15
 	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tse/WangSWLSDYL15},
 	bibsource = {dblp computer science bibliography, http://dblp.org},
 }
+
+@inproceedings{DBLP:conf/concur/CassezDFLL05,
+  author       = {Franck Cassez and
+                  Alexandre David and
+                  Emmanuel Fleury and
+                  Kim Guldstrand Larsen and
+                  Didier Lime},
+  editor       = {Martín Abadi and
+                  Luca de Alfaro},
+  title        = {Efficient On-the-Fly Algorithms for the Analysis of Timed Games},
+  booktitle    = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,
+                  {CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {3653},
+  pages        = {66--80},
+  publisher    = {Springer},
+  year         = {2005},
+  url          = {https://doi.org/10.1007/11539452\_9},
+  doi          = {10.1007/11539452\_9},
+  timestamp    = {Tue, 14 May 2019 10:00:43 +0200},
+  biburl       = {https://dblp.org/rec/conf/concur/CassezDFLL05.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/wodes/JovanovicFLR12,
+  author       = {Aleksandra Jovanovic and
+                  Sébastien Faucou and
+                  Didier Lime and
+                  Olivier H. Roux},
+  editor       = {Antonio Ramírez-Treviño and
+                  Ernesto López-Mellado and
+                  Jean-Jacques Lesage and
+                  Manuel Silva Suárez},
+  title        = {Real-time control with parametric timed reachability games},
+  booktitle    = {11th International Workshop on Discrete Event Systems, {WODES} 2012,
+                  Guadalajara, Mexico, October 3-5, 2012},
+  pages        = {323--330},
+  publisher    = {International Federation of Automatic Control},
+  year         = {2012},
+  url          = {https://doi.org/10.3182/20121003-3-MX-4033.00052},
+  doi          = {10.3182/20121003-3-MX-4033.00052},
+  timestamp    = {Wed, 26 Jan 2022 14:16:09 +0100},
+  biburl       = {https://dblp.org/rec/conf/wodes/JovanovicFLR12.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}