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

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Mon Aug 10 14:50:11 2009 +0200

Improved BagnaraHZ09TCS and BagnaraHZ09FMSD. Added BagnaraHZ09TRb.

---

htdocs/Documentation/BagnaraHZ09TRb.pdf | Bin 0 -> 346789 bytes htdocs/Documentation/ppl.bib | 48 +++++++++++++++++++++++++++--- 2 files changed, 43 insertions(+), 5 deletions(-)

diff --git a/htdocs/Documentation/BagnaraHZ09TRb.pdf b/htdocs/Documentation/BagnaraHZ09TRb.pdf new file mode 100644 index 0000000..d4c6300 Binary files /dev/null and b/htdocs/Documentation/BagnaraHZ09TRb.pdf differ diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 54a6121..27cec84 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -904,7 +904,7 @@ Journal = "Formal Methods in System Design", Publisher = "Springer-Verlag, Berlin", Year = 2009, - Note = "Available online at + Note = "To appear in print. Available online at \url{http://www.springerlink.com/content/d40842574t1r5877/%7D", Abstract = "Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is @@ -943,10 +943,11 @@ Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit`a di Parma, Italy", Year = 2009, - Note = "Available at \url{http://www.cs.unipr.it/Publications/%7D. - An improved version (typos corrected in statement and proof - of Theorem~6.8) has been published as {\tt arXiv:cs.CG/0904.1783}, - available from \url{http://arxiv.org/%7D.", + Note = "Available at \url{http://www.cs.unipr.it/Publications/%7D. A + corrected and improved version (corrected an error in the + statement of condition (3) of Theorem~3.6, typos corrected + in statement and proof of Theorem~6.8) has been published + in \cite{BagnaraHZ09TRb}.", Abstract = "Deciding whether the union of two convex polyhedra is a convex polyhedron is a basic problem in polyhedral computation having important applications in the field @@ -975,6 +976,43 @@ URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TRa.pdf" }

+@Misc{BagnaraHZ09TRb, + Author = "R. Bagnara and P. M. Hill and E. Zaffanella", + Title = "Exact Join Detection for Convex Polyhedra + and Other Numerical Abstractions", + Howpublished = "Report {\tt arXiv:cs.CG/0904.1783}", + Year = 2009, + Note = "Available at \url{http://arxiv.org/%7D + and \url{http://www.cs.unipr.it/ppl/%7D", + Abstract = "Deciding whether the union of two convex polyhedra is + itself a convex polyhedron is a basic problem in + polyhedral computations; having important applications + in the field of constrained control and in the + synthesis, analysis, verification and optimization of + hardware and software systems. In such application + fields though, general convex polyhedra are just one + among many, so-called, \emph{numerical abstractions}, + which range from restricted families of (not necessarily + closed) convex polyhedra to non-convex geometrical + objects. We thus tackle the problem from an abstract + point of view: for a wide range of numerical + abstractions that can be modeled as bounded + join-semilattices ---that is, partial orders where any + finite set of elements has a least upper bound---, we + show necessary and sufficient conditions for the + equivalence between the lattice-theoretic join and the + set-theoretic union. For the case of closed convex + polyhedra ---which, as far as we know, is the only one + already studied in the literature--- we improve upon the + state-of-the-art by providing a new algorithm with a + better worst-case complexity. The results and + algorithms presented for the other numerical + abstractions are new to this paper. All the algorithms + have been implemented, experimentally validated, and + made available in the Parma Polyhedra Library.", + URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TRb.pdf" +} + @InProceedings{BalasundaramK89, Author = "V. Balasundaram and K. Kennedy", Title = "A Technique for Summarizing Data Access