💻 computer science

Event Calculus Meets Hybrid ASP

This paper introduces Hybrid Event Calculus, an extended axiomatization implemented in Hybrid ASP systems (clingcon and clingo-lpx) that overcomes the scalability and accuracy limitations of traditional grounding-based and top-down approaches by representing continuous changes and dense domains as linear constraints, thereby enabling accurate and scalable modeling of safety-critical systems.

Original authors: Ondřej Vašíček, Joaquín Arias, Jan Fiedor, Gopal Gupta, Bohuslav Křena, Jakub Němec, Javier Romero, Tomáš Vojnar

Published 2026-06-04

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Ondřej Vašíček, Joaquín Arias, Jan Fiedor, Gopal Gupta, Bohuslav Křena, Jakub Němec, Javier Romero, Tomáš Vojnar

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to write a story about a complex machine, like a self-driving car or a smart thermostat. You want to describe how it behaves over time: what happens when a button is pressed, how the temperature changes, and when the system should sound an alarm.

In the world of computer science, there is a language called Event Calculus that is great for writing these stories because it feels very close to how humans speak. However, when computers try to read these stories, they hit a wall if the story involves continuous change (like a temperature slowly dropping) or huge ranges of numbers (like time measured in milliseconds over years).

This paper introduces a new way to tell these stories, called Hybrid Event Calculus, which acts like a "super-charged" translator for computers. Here is how it works, using some everyday analogies:

1. The Problem: The "Pixelated" Map

Traditional computer methods for checking these stories (called Discrete Event Calculus) work like a low-resolution, pixelated map.

The Issue: If you want to track a ball falling, a pixelated map can only show the ball at specific grid points (e.g., 1 meter, 2 meters, 3 meters). It misses what happens between the grids.
The Explosion: To make the map more accurate, you have to add more pixels. But if you want to track time down to the millisecond for a whole day, the number of pixels becomes so huge that the computer's memory explodes, and it crashes. It's like trying to count every single grain of sand on a beach to find one specific shell.

2. The Solution: The "Smart Sketch" (Hybrid ASP)

The authors created a new method called Hybrid Event Calculus. Instead of drawing every single pixel, this method uses a "Smart Sketch" approach.

Functional Fluents (The Variable Paint): Instead of saying "The temperature is 20" or "The temperature is 21," the computer treats the temperature as a flexible variable, like a paintbrush that can be anywhere on the canvas. It uses math constraints (like a ruler) to define the range, rather than listing every single number.
Abstract Steps (The Story Beats): Instead of forcing the story to happen at every single second (1:00, 1:01, 1:02), the computer only looks at the important moments (the "beats" of the story).
- Example: If a ball is dropped, the computer only cares about the moment it is dropped and the moment it hits the ground. It ignores the millions of tiny moments in between, calculating the path mathematically instead of listing them one by one.

3. The Engine: The "Mathematical Librarian"

To make this work, the authors used special computer tools (called clingcon and clingo-lpx) that act like a librarian who is also a mathematician.

The Old Way: The computer would try to read every single book in the library (grounding every possibility) before answering a question.
The New Way: The computer asks the mathematician-librarian, "If the ball falls at speed X, where will it be at time Y?" The librarian solves the math instantly without needing to look up every single second in a book. This allows the system to handle dense domains (infinite possibilities between numbers) without getting overwhelmed.

4. Why It Matters: Accuracy Without the Crash

The paper shows that this new method has two superpowers:

It doesn't care about size: Whether you are tracking time for 10 seconds or 10 years, the computer's workload stays the same because it only counts the "story beats," not the seconds.
It handles the "in-between": Because it uses math constraints (specifically rational numbers), it can accurately model continuous changes. It can tell you exactly when a falling object hits the ground, even if that happens at a time that isn't a whole number (like 10.5 seconds), which the old "pixelated" methods often miss or get wrong.

Summary

Think of the old method as trying to watch a movie by looking at a flipbook where you have to draw every single frame manually. If the movie is long, you run out of paper.

The new Hybrid Event Calculus is like watching the movie on a high-definition screen. You only pause at the key scenes (the events), and the computer fills in the smooth motion between them using math. This lets you analyze complex, real-world systems (like safety-critical machines) accurately, without the computer getting bogged down by the sheer amount of data.

Technical Summary: Event Calculus Meets Hybrid ASP

Problem Statement

Event Calculus (EC) is a logical formalism well-suited for specifying safety-critical cyber-physical systems (CPS) due to its semantic proximity to natural language and its ability to model both discrete and continuous changes. However, applying EC to real-world CPS specifications faces significant challenges when dealing with continuous changes and large or dense value domains for time and system properties (fluents).

Current state-of-the-art reasoning tools based on Answer Set Programming (ASP) struggle with these requirements:

Grounding-based solvers (e.g., clingo): These require the discretization of dense domains. While increasing precision (e.g., from seconds to milliseconds) can mitigate representation inaccuracies, it leads to a combinatorial explosion in the size of the grounded program, causing solvers to run out of memory or time.
Grounding-free solvers (e.g., s(CASP)): While these avoid discretization and the grounding explosion, they rely on top-down execution which can suffer from non-termination issues and lack the optimized performance of modern grounding-based solvers.

Consequently, there is a gap in tools capable of accurately modeling continuous change in EC without sacrificing scalability or termination guarantees.

Methodology: Hybrid Event Calculus (HEC)

The authors introduce Hybrid EC, an extended axiomatization of Discrete Event Calculus (DEC), designed to address these limitations. The approach leverages Hybrid ASP, a paradigm that combines standard ASP with linear constraints over integers and rationals.

The core technical innovations of Hybrid EC include:

1. Functional Fluents

Unlike standard DEC, which uses relational fluents (true/false at a timepoint), Hybrid EC introduces functional fluents. The values of these fluents are represented as symbolic terms (e.g., (F, S)) whose values are determined by linear constraints rather than explicit grounding. This allows fluents to hold dense values without requiring a ground atom for every possible value.

2. Hybrid Representation of Time

DEC operates on integer time steps ( $T, T+1$ ). Hybrid EC replaces this with abstract step indices ( $S, S+1$ ) representing the sequence of system evolution.

Discrete Steps: Only the sequence of events is grounded as discrete steps.
Dense Time: The actual time associated with each step is handled by a constraint solver via theory atoms (e.g., (time, S)).
Mapping: Observations of events at specific timepoints $T$ are mapped to abstract steps $S$ via constraints, ensuring that the grounding size depends on the number of events, not the size of the time domain.

3. Axiomatization (HEC)

The authors extend the DEC axioms (specifically those by Lee and Palla, 2012) to accommodate functional fluents and the hybrid time representation. Key adaptations include:

Inertia and Event Effects: Rules are modified to assign values to functional fluents using linear expressions (e.g., &sum{(F,S)} = (F,S+1)) unless an event initiates a new value or releases the fluent from inertia.
Continuous Change: Trajectories are redefined to calculate fluent values based on the actual time difference between steps ( $R \times ((time, S_1+S_2) - (time, S_1))$ ) rather than discrete step counts, enabling accurate modeling of monotonic linear continuous change.
Triggered Events: To handle events triggered by continuous change (e.g., hitting the ground), the system employs no_jump constraints. These prevent steps from "skipping" over critical values (like zero height) in monotonic changes, ensuring the trigger condition is met exactly.

4. Implementation and Solving

The implementation utilizes two Hybrid ASP solvers:

clingcon: Supports linear constraints over integers.
clingo-lpx: Supports linear constraints over rationals.

The system uses an incremental solving approach. It starts with a minimal number of steps and iteratively increases the step count until a model is found. This avoids the need for the user to guess the correct number of steps. The approach ensures termination whenever a solution exists within the defined step bounds.

Key Contributions

Hybrid EC Axiomatization: A formal extension of DEC that integrates functional fluents and abstract step-based time mapping, allowing for the representation of dense domains without grounding explosion.
Accurate Continuous Modeling: By utilizing clingo-lpx and rational numbers, the approach enables accurate reasoning about continuous change (dense time and values), a capability previously unavailable in standard ASP-based EC implementations without discretization artifacts.
Scalability: The grounding size is decoupled from the size of the time and value domains, depending instead on the number of events. This allows the system to handle large domains efficiently.
Dual Implementation: The authors provide implementations using both integer (clingcon) and rational (clingo-lpx) solvers, demonstrating the flexibility of the approach.

Experimental Results

The authors evaluated the approach on over 30 benchmark problems from the literature (e.g., counter, falling object, stolen car, hot air balloon).

Expressiveness: The Hybrid EC implementations (clingcon and clingo-lpx) successfully solved all problems handled by the standard clingo (DEC) implementation. Furthermore, clingo-lpx successfully solved problems requiring continuous change (dense domains), which clingo and clingcon could not handle accurately.
Scalability (Domain Size): Experiments varying the size of time and value domains showed that clingo's execution time increased exponentially (leading to timeouts) as domain size grew. In contrast, clingcon and clingo-lpx maintained stable execution times, unaffected by the domain size.
Scalability (Event Count): Performance scaled linearly with the number of events, confirming that the approach is driven by the number of events rather than the domain magnitude.
Rational vs. Integer: The use of rationals in clingo-lpx did not negatively impact scalability compared to integer reasoning, while providing the necessary precision for continuous modeling.

Significance and Claims

The paper claims that Hybrid EC successfully bridges the gap between the semantic richness of Event Calculus and the computational limitations of current ASP solvers.

Accuracy: It eliminates inaccuracies caused by discretization, allowing for faithful modeling of continuous physical processes.
Efficiency: It avoids the grounding explosion associated with large or dense domains, making rigorous verification of complex CPS specifications feasible.
Termination: Unlike grounding-free query-driven approaches, the Hybrid ASP approach ensures termination for solvable instances.

The authors note that while the current implementation handles monotonic linear changes, reasoning about dense time introduces challenges such as Zeno behavior. They acknowledge that addressing these specific phenomena in the context of HEC is left for future work, though they provide encodings for related problems. The work establishes a foundation for using Hybrid ASP to reason about safety-critical systems with continuous dynamics.