Timed Model-Checking Game Case of Event-Recording Logic

ABSTRACT. We consider the model-checking problem for a weak real-time logic called event-recording logic. We propose a two players parity game which decides if a real-time system modelled with an event-recording automaton is a model of a given formula '. Region abstraction is done on the positions of the game in order to compute a winning strategy in that game. We show that a real-time system is a model of a formula if there is a winning strategy for one player in the game. RÉSUMÉ. Nous traitons le problème de model-checking pour une logique temps réelle faible appelée event-recording logic. Les systèmes temps réels considérés sont modélisés à l’aide des systèmes de transition temporisés sans mémoires qui dérivent des event-recording automata. Nous proposons un jeu de parité à deux joueurs et nous montrons qu’un système est un modèle de notre formule s’il existe une stratégie gagnante pour un joueur déterminé dans le jeu. Le calcul d’une stratégie gagnante est rendu possible par l’abstraction de l’espace des positions du jeu à l’aide des régions