doc. Dipl.-Ing. Dr. techn. Stefan Ratschan

Stať ve sborníku

10.1007/978-3-031-27481-7_5

Katedra číslicového návrhu

Railway scheduling is a problem that exhibits both non- trivial discrete and continuous behavior. In this paper, we model this problem using a combination of SAT and ordinary differential equations (SAT modulo ODE). In addition, we adapt our existing method for solv- ing such problems in such a way that the resulting solver is competitive with methods based on dedicated railway simulators while being more general and extensible.

Stať ve sborníku

10.1007/978-3-030-50995-8_5

Katedra číslicového návrhu

Differential equations are of immense importance for modeling physical phenomena, often in combination with discrete modeling formalisms. In current industrial practice, properties of the resulting models are checked by testing, using simulation tools. Research on SAT solvers that are able to handle differential equations has aimed at replacing tests by correctness proofs. However, there are fundamental limitations to such approaches in the form of undecidability, and moreover, the resulting solvers do not scale to problems of the size commonly handled by simulation tools. Also, in many applications, classical mathematical semantics of differential equations often does not correspond well to the actual intended semantics, and hence a correctness proof wrt. mathematical semantics does not ensure correctness of the intended system. In this paper, we head at overcoming those limitations by an alternative approach to handling differential equations within SAT solvers. This approach is usually based on the semantics used by tests in simulation tools, but still may result in mathematically precise correctness proofs wrt. that semantics. Experiments with a prototype implementation confirm the promise of such an approach.