The railroad crossing problem: Towards semantics of timed algorithms and their model checking in high level languages

Abstract

The goal of this paper is to analyse semantics of algorithms with explicit continuous time with further aim to find approaches to automatize model checking in high level, easily understandable languages. We give here a general notion of timed transition system and its formula representation that are sufficient to deal with some known examples of timed algorithms. We prove that the general semantics gives the same executions as direct, more intuitive interpretations of executions of algorithms. In a way, we try to give a general treatment of considerations of Yu.Gurevich and his co-authors concerning concrete Gurevich machines (called evolving algebras in [Gur95]), in particular, related to Railroad Crossing Problem [GH96]. Besides that we formalize specifications of this problem in a high level language which permits to rewrite directly natural language formulations, and to give a formal proof of correctness of the railroad crossing algorithm using rather a small amount of logical means, and this leads to hypotheses how automatize inference search.