Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R)

Timed automata has been used as a powerful formalism for specifying, designing, and analyzing real time systems. We consider the generalization of timed automata to Pushdown Timed Automata (PTA). We show how PTAs can be elegantly modeled via logic programming extended with coinduction and constraints over reals. We use this logic programming realization of a PTA to develop an elegant solution to the generalized railroad crossing problem of Lynch and Heitmeyer. Interesting properties of the system can be verified merely by posing appropriate queries to this coinductive constraint logic program.

• Type: Conference
• Year: 2010
• Where: LATA
• Authors: Neda Saeedloei and Gopal Gupta
• Keywords: Automata Theory, LATA 2010