@InProceedings{EggKalKupTei:RAC08:Challenges,
author =        "Andreas Eggers and
                 Natalia Kalinnik and
                 Stefan Kupferschmid and
                 Tino Teige",
title =         "Challenges in Constraint-Based Analysis of Hybrid Systems",
booktitle =     "Recent Advances in Constraints --
                 13th Annual ERCIM International Workshop on Constraint Solving
                 and Constraint Logic Programming, CSCLP 2008, Rome, Italy, June
                 18-20, 2008, Revised Selected Papers",
editor =        "Angelo Oddi and Fran\c{c}ois Fages and Francesca Rossi",
publisher =     "Springer",
address =       "Berlin, Heidelberg",
series =        "Lecture Notes in Artificial Intelligence",
volume =        "5655",
pages =         "51--65",
year =          "2009",
doi =           "10.1007/978-3-642-03251-6_4",
note =          "Springerlink:
                 \url{http://www.springerlink.com/content/hx755817464v6746}",
bibtex =        "eggers.rac08.bib",
pdf =           "eggers.rac08.pdf",
subproject=    {H1/2},
access =        "restricted",
abstract =      "In the analysis of hybrid discrete-continuous systems, rich
                 arithmetic constraint formulae with complex Boolean structure
                 arise naturally. The iSAT algorithm, a solver for such
                 formulae, is aimed at bounded model checking of hybrid systems.
                 In this paper, we identify challenges emerging from planned and
                 ongoing work to enhance the iSAT algorithm. First, we propose
                 an extension of iSAT to directly handle ordinary differential
                 equations as constraints. Second, we outline the recently
                 introduced generalization of the iSAT algorithm to deal with
                 probabilistic hybrid systems and some open research issues in
                 that context.  Third, we present ideas on how to move from
                 bounded to unbounded model checking by using the concept of
                 interpolation. Finally, we discuss the adaption of some
                 parallelization techniques to the iSAT case, which will
                 hopefully lead to performance gains in the future. By
                 presenting these open research questions, this paper aims at
                 fostering discussions on these extensions of constraint
                 solving.",
keywords =      "mixed Boolean and arithmetic constraints - differential
                 equations - stochastic SMT - Craig interpolation - parallel
                 solver "
}