Saeedloei, Neda; Gupta, Gopal Verifying complex continuous real-time systems with coinductive CLP(R). (English) Zbl 1284.68365 Dediu, Adrian-Horia (ed.) et al., Language and automata theory and applications. 4th international conference, LATA 2010, Trier, Germany, May 24–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13088-5/pbk). Lecture Notes in Computer Science 6031, 536-548 (2010). Summary: Timed automata have 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 PTA can be elegantly modeled via logic programming extended with co-induction and constraints over reals. We propose a general framework based on constraint logic programming and co-induction for modeling/verifying real-time systems. We use this framework 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.For the entire collection see [Zbl 1187.68004]. Cited in 4 Documents MSC: 68Q45 Formal languages and automata 68N17 Logic programming 68Q60 Specification and verification (program logics, model checking, etc.) Software:Uppaal PDFBibTeX XMLCite \textit{N. Saeedloei} and \textit{G. Gupta}, Lect. Notes Comput. Sci. 6031, 536--548 (2010; Zbl 1284.68365) Full Text: DOI