On Zeno-like Behaviors in the Event Calculus with Goal-directed Answer Set Programming
It has been argued that Event Calculus (EC) is suitable for modeling high-level specifications of safety-critical cyber-physical systems. The primary advantage lies in the rather small semantic gap between EC models and requirements expressed in a semi-formal natural language. Moreover, its use of continuous time and variables avoids imprecision that stems from discretization. In the past, we have shown that a goal-directed ASP system can be used for implementing these EC models. However, precise representation of time as an infinitesimally divisible continuous quantity leads to Zeno-like behaviors and to non-termination in such a system. In this work, we model a number of well-known example problems from the literature to systematically study various natural EC modeling patterns that yield these Zeno-like behaviors, and propose ways to deal with them. Moreover, we also propose a technique to automatically detect all such cases.
Authors
- Ondřej Vašíček (ORCID: https://orcid.org/0000-0002-4944-2198)
- Bohuslav Křena (ORCID: https://orcid.org/0000-0001-9572-1799)
- Jan Fiedor
- Gopal Gupta
- Tomáš Vojnar
- Brendan P. Hall
- Joaquin Arias
- Brian Larson
Institutions
- The University of Texas at Dallas (US)
- Universidad Rey Juan Carlos (ES)
- Masaryk University (CZ)
- Ardent Sound (United States) (US)
- Brno University of Technology (CZ)
- Honeywell (United States) (US)
Publication Details
- Journal
- Electronic Proceedings in Theoretical Computer Science
- Published
- 2026-01-08
- DOI
- https://doi.org/10.4204/eptcs.439.34
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- National Science Foundation
- European Commission
- Grantová Agentura České Republiky
- University of Texas at Dallas
- European Regional Development Fund
- Agencia Estatal de Investigación