From 76f61acc6342b98d1202b1e319dc88f6491f1d85 Mon Sep 17 00:00:00 2001 From: mikaelbdj Date: Sun, 12 Nov 2023 23:08:40 +0100 Subject: [PATCH] Add PTG things to manual --- doc/IMITATOR-user-manual.tex | 27 ++++++++++++++++++++-- doc/biblio.bib | 45 ++++++++++++++++++++++++++++++++++++ 2 files changed, 70 insertions(+), 2 deletions(-) diff --git a/doc/IMITATOR-user-manual.tex b/doc/IMITATOR-user-manual.tex index 6aa615ae..94032bbe 100644 --- 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 index 6063698f..03826525 100644 --- 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} +} \ No newline at end of file