Module: ppl/ppl Branch: master Commit: 81b01e9b60766bec50569a1ef68dc22d70de0a65 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=81b01e9b60766...
Author: Roberto Bagnara roberto.bagnara@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." }
-@Article{BenerecettiFM12, +@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,