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 systems. this paper, we identify challenges emerging from planned and ongoing work to enhance algorithm. First, propose an extension directly handle ordinary differential equations as constraints. Second, outline recently introduced generalization algorithm deal probabilistic systems some open research issues in that context. Third, present ideas on how move unbounded by using concept interpolation. Finally, discuss adaption parallelization techniques case, which will hopefully lead performance gains future. By presenting these questions, paper aims fostering discussions extensions solving.