[PPL-devel] [GIT] ppl/ppl(master): BenerecettiFM13 has been published.

[Roberto Bagnara]

Module: ppl/ppl
Branch: master
Commit: 81b01e9b60766bec50569a1ef68dc22d70de0a65
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=81b01e9b60766bec50569a1ef68dc22d70de0a65

Author: Roberto Bagnara <roberto.bagnara at bugseng.com>
Date:   Mon Oct 28 09:03:22 2013 +0100

BenerecettiFM13 has been published.

---

 doc/definitions.dox |   45 ++++++++++++++++++++++++---------------------
 doc/ppl.bib         |   26 ++++++++++++++++++++++++--
 2 files changed, 48 insertions(+), 23 deletions(-)

diff --git a/doc/definitions.dox b/doc/definitions.dox
index b5c6007..eae3ce5 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -3070,6 +3070,30 @@ R. Bagnara, K. Dobson, P. M. Hill, M. Mundell, and E. Z
 </DD>
 
 
+<DT>[BFM11]</DT>
+<DD>
+\anchor BFM11
+M. Benerecetti, M. Faella, and S. Minopoli.
+ Towards efficient exact synthesis for linear hybrid systems.
+ In <em>Proceedings of 2nd International Symposium on Games,
+  Automata, Logics and Formal Verification (GandALF 2011)</em>, volume 54 of <em>
+  Electronic Proceedings in Theoretical Computer Science</em>, pages 263-277,
+  Minori, Amalfi Coast, Italy, 2011.
+
+</DD>
+
+
+<DT>[BFM13]</DT>
+<DD>
+\anchor BFM13
+M. Benerecetti, M. Faella, and S. Minopoli.
+ Automatic synthesis of switching controllers for linear hybrid
+  systems: Safety control.
+ <em>Theoretical Computer Science</em>, 493:116-138, 2013.
+
+</DD>
+
+
 <DT>[BFT00]</DT>
 <DD>
 \anchor BFT00
@@ -3542,27 +3566,6 @@ R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill.
 </DD>
 
 
-<DT>[BFM11]</DT>
-<DD>
-\anchor BFM11
-M. Benerecetti, M. Faella, and S. Minopoli.
-  Towards efficient exact synthesis for Linear Hybrid Systems.
- In <em>Proceedings of the 2nd International Symposium on Games,
-               Automata, Logics and Formal Verification (GandALF 2011)</em>,
-  volume 54 of <em>Electronic Proceedings in Theoretical Computer Science</em>,
-  pages 263-277.
-</DD>
-
-
-<DT>[BFM12]</DT>
-<DD>
-\anchor BFM12
-M. Benerecetti, M. Faella, and S. Minopoli.
- Automatic synthesis of switching controllers for Linear Hybrid Systems: safety control.
- <em>Theoretical Computer Science</em>, Elsevier. To appear.
-</DD>
-
-
 <DT>[CC76]</DT>
 <DD>
 \anchor CC76
diff --git a/doc/ppl.bib b/doc/ppl.bib
index 02d4d18..cbb16bb 100644
--- a/doc/ppl.bib
+++ b/doc/ppl.bib
@@ -1249,12 +1249,34 @@ Summarizing:
               top of the tool PHAVer."
 }
 
- at Article{BenerecettiFM12,
+ at Article{BenerecettiFM13,
   Author = "M. Benerecetti and M. Faella and S. Minopoli",
   Title = "Automatic Synthesis of Switching Controllers for Linear Hybrid Systems: Safety Control",
   Journal = "Theoretical Computer Science",
+  Volume = 493,
+  Pages = "116--138",
   Publisher = "Elsevier",
-  Notes = "To appear"
+  Year = 2013,
+  Abstract = "In this paper we study the problem of automatically
+              generating switching controllers for the class of Linear
+              Hybrid Automata, with respect to safety
+              objectives. While the same problem has been already
+              considered in the literature, no sound and complete
+              solution has been provided so far. We identify and solve
+              inaccuracies contained in previous characterizations of
+              the problem, providing a sound and complete symbolic
+              fixpoint procedure to compute the set of states from
+              which a controller can keep the system in a given set of
+              desired states. While the overall procedure may not
+              terminate, we prove the termination of each iteration,
+              thus paving the way to an effective implementation.  The
+              techniques needed to effectively and efficiently
+              implement the proposed solution procedure, based on
+              polyhedral abstractions of the state space, are
+              thoroughly illustrated and discussed. Finally, some
+              supporting and promising experimental results, based on
+              the implementation of the proposed techniques on top of
+              the tool PHAVer, are presented."
 }
 
 @InProceedings{BessonJT99,