summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/definitions.dox45
-rw-r--r--doc/ppl.bib26
2 files changed, 48 insertions, 23 deletions
diff --git a/doc/definitions.dox b/doc/definitions.dox
index b5c600777..eae3ce50b 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.&nbsp;Benerecetti, M.&nbsp;Faella, and S.&nbsp;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&nbsp;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.&nbsp;Benerecetti, M.&nbsp;Faella, and S.&nbsp;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.&nbsp;Bagnara, E.&nbsp;Ricci, E.&nbsp;Zaffanella, and P.&nbsp;M. Hill.
</DD>
-<DT>[BFM11]</DT>
-<DD>
-\anchor BFM11
-M.&nbsp;Benerecetti, M.&nbsp;Faella, and S.&nbsp;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.&nbsp;Benerecetti, M.&nbsp;Faella, and S.&nbsp;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 02d4d180b..cbb16bbda 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,