Challenges in Constraint-Based Analysis of Hybrid Systems

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 ...

• Type: Conference
• Year: 2008
• Where: CSCLP
• Authors: Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige
• Keywords: Artificial Intelligence, CSCLP 2008, Hybrid Systems, ISAT Algorithm, Model Checking