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

Institutions

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

Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

On Zeno-like Behaviors in the Event Calculus with Goal-directed Answer Set Programming

Ondřej Vašíček, Bohuslav Křena, Jan Fiedor, Gopal Gupta et al.
Electronic Proceedings in Theoretical Computer Science
Formal Methods in Verification
article

On Zeno-like Behaviors in the Event Calculus with Goal-directed Answer Set Programming

Ondřej Vašíček, Bohuslav Křena, Jan Fiedor, Gopal Gupta, Tomáš Vojnar, Brendan P. Hall, Joaquin Arias, Brian Larson
article en

Abstract

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.

Electronic Proceedings in Theoretical Computer ScienceVol. 439
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)
National Science Foundation, European Commission, Grantová Agentura České Republiky, University of Texas at Dallas, European Regional Development Fund, Agencia Estatal de Investigación
Peace, Justice and strong institutions
Openalex Percentile: Top 92%
Formal Methods in Verification
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

On Zeno-like Behaviors in the Event Calculus with Goal-directed Answer Set Programming — Ondřej Vašíček, Bohuslav Křena, et al. · Electronic Proceedings in Theoretical Computer Science (2026) | TGRS Research Map | TGRS