pith. sign in

arxiv: 2606.04905 · v1 · pith:3Q442GLOnew · submitted 2026-06-03 · 💻 cs.LO

Event Calculus Meets Hybrid ASP

Pith reviewed 2026-06-28 03:44 UTC · model grok-4.3

classification 💻 cs.LO
keywords event calculushybrid answer set programmingcontinuous changefunctional fluentslinear constraintssafety-critical systemsdense domainsclingo-lpx
0
0 comments X

The pith

Hybrid Event Calculus uses functional fluents and abstract time steps to model continuous change accurately in hybrid ASP solvers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Hybrid EC as an extension of Discrete Event Calculus that adds functional fluents and maps time to abstract steps. This allows implementation in hybrid ASP systems such as clingcon and clingo-lpx, where domains of fluents and time are represented as linear constraints solved externally. The approach avoids combinatorial explosion from grounding and non-termination from top-down execution while preserving termination when solutions exist. A sympathetic reader would care because it supports precise specification of safety-critical systems involving continuous dynamics without inaccuracy from discretization. Validation shows the implementations scale independently of domain size and that clingo-lpx's dense domain handling enables accurate continuous change modeling.

Core claim

Hybrid EC extends the axiomatization of DEC via functional fluents and a mapping of time to abstract steps. Implemented in clingcon and clingo-lpx, value domains are represented as linear constraints evaluated by external solvers. This guarantees termination whenever solutions exist and is unaffected by the size of the domains, with clingo-lpx enabling accurate modeling of continuous change through dense domains.

What carries the argument

Hybrid EC axiomatization that adds functional fluents and maps time to abstract steps, with domains encoded as linear constraints solved by external hybrid ASP engines.

If this is right

  • Both implementations remain unaffected by the size of the domains.
  • Handling rationals does not impact scalability.
  • The ability of clingo-lpx to handle dense domains enables accurate modeling of continuous change.
  • Termination is guaranteed whenever solutions exist.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach may apply to verification of other hybrid systems beyond the tested examples by swapping in additional constraint solvers.
  • Abstract time mapping could support combined discrete-continuous modeling when linked to existing discrete event frameworks.
  • Semantic preservation opens the possibility of using natural-language-style requirements directly for continuous dynamics without manual discretization.

Load-bearing premise

The mapping of time to abstract steps together with functional fluents preserves the original Event Calculus semantics for continuous change while guaranteeing termination when solutions exist.

What would settle it

A concrete continuous-change scenario where the hybrid implementation yields a result differing from the original Event Calculus axioms or fails to terminate despite an existing solution.

Figures

Figures reproduced from arXiv: 2606.04905 by Bohuslav K\v{r}ena, Gopal Gupta, Jakub N\v{e}mec, Jan Fiedor, Javier Romero, Joaqu\'in Arias, Ond\v{r}ej Va\v{s}\'i\v{c}ek, Tom\'a\v{s} Vojnar.

Figure 1
Figure 1. Figure 1: DEC encoding of the counter example. Example 1 (Counter 1 ) Consider the example from Mueller (2008) that models a counter that can be incremented or reset. Figure 1a models a fragment (omitting the reset) of the rules of the domain, defining the fluent val(V), the inc event, and its conditional effects on the fluent. Then, Figure 1b models the narrative of initial observations and event occurrences. For t… view at source ↗
Figure 2
Figure 2. Figure 2: Mapping of (dense) time values to discrete steps. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Axioms of HEC 5 and HEC 9 representing event effects and inertia. initiated or released from inertia. Line 7 of HEC 9 represents the effect of initiating fluent F whenever event E happens at step S. The corresponding theory atom assigns to fluent F at step S+1 the value of the linear expression LE, given by a new predicate initiates/4. A linear expression c1*v1+...+cN*vN is encoded as a tuple ((c1,v1),...,… view at source ↗
Figure 4
Figure 4. Figure 4: Axioms for representing gradual (DEC) and continuous (HEC) change. is a key difference because the value assigned by the trajectory to F2 cannot be derived directly from the step-based duration, as the result would vary if additional steps are inserted (e.g., due to an unrelated event occurring during the trajectory). Therefore, the theory atom in the head represents the linear expression LE as in HEC 9 (u… view at source ↗
Figure 5
Figure 5. Figure 5: Non-event observations. mapped to step S but F does not hold at S. Other observations of relational fluents are encoded analogously.8 For functional fluents, the auxiliary predicate in_ttory(F,S,R), defined in lines 12-13, identifies the case where fluent F is under a trajectory at step S, and extracts the rate of change R. If no trajectory applies to F at step S, the situation is analogous to relational f… view at source ↗
Figure 6
Figure 6. Figure 6: The no_jump constraint and a triggered event for the falling object. The above is a common problem in hybrid systems and can be addressed using a constraint that prevents steps from jumping over particular values of interest when deal￾ing with monotonic changes, as was discussed by Shin and Davis (2005) for SAT-based planning. In our case, this is relevant for events triggered based on continuous change of… view at source ↗
Figure 7
Figure 7. Figure 7: The significant step constraint. Our implementation uses an incremental execution approach to find the right number of steps automatically. A limitation of this approach is that it currently is not possible to automatically identify that there is no model for any number of steps. Instead, the script currently explores up to a given maximum number of steps as defined by the user. 5 Accurately Representing C… view at source ↗
read the original abstract

Event Calculus (EC) implemented in answer set programming (ASP) has proven suitable for specifying requirements on safety-critical systems thanks to its elegant representation of both discrete and continuous changes and its semantic closeness to semi-formal natural language. However, continuous changes and the size of value domains of time and system properties (fluents) pose significant challenges. Grounding-based ASP solvers, e.g., clingo, which implement Discrete EC (DEC), lead to combinatorial explosion in program size and inaccurate representation. The grounding-free s(CASP) does not discretize but struggles with non-termination due to its top-down execution. This paper introduces Hybrid EC, an extended axiomatization of DEC, that tackles the challenges via functional fluents and a mapping of time to abstract steps. We implement it using clingcon and clingo-lpx (Hybrid ASP systems over integers and rationals, respectively) where the value (dense) domains of fluents and time are represented as linear constraints and evaluated by external solvers, while ensuring termination whenever solutions exist. We validate both implementations on a number of examples and observe that they are unaffected by the size of the domains and that handling rationals does not impact scalability. Most importantly, the ability of clingo-lpx to handle dense domains enables accurate modeling of continuous change.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper claims that Hybrid Event Calculus (an extension of Discrete EC) using functional fluents and a mapping of time to abstract steps, when implemented in Hybrid ASP solvers clingcon and clingo-lpx, avoids grounding explosion, guarantees termination when solutions exist, remains unaffected by domain size, and enables accurate continuous-change modeling via dense rational domains in clingo-lpx, as shown by validation on examples.

Significance. If the encoding is shown to preserve EC semantics, the approach would provide a practical route to scalable, termination-guaranteed reasoning over continuous dynamics in answer-set programming, strengthening its applicability to safety-critical system specification.

major comments (1)
  1. [Hybrid EC axiomatization and implementation description] The central claim that clingo-lpx enables accurate continuous-change modeling rests on the assertion that the Hybrid EC axiomatization (functional fluents plus time-to-abstract-steps mapping) preserves the trajectories of standard Event Calculus on dense time while guaranteeing termination. No equivalence theorem, model-theoretic correspondence, or bisimulation argument is supplied; validation is limited to examples. This is load-bearing for the accuracy claim.

Simulated Author's Rebuttal

1 responses · 1 unresolved

We thank the referee for the constructive feedback on our manuscript. We address the major comment point by point below.

read point-by-point responses
  1. Referee: [Hybrid EC axiomatization and implementation description] The central claim that clingo-lpx enables accurate continuous-change modeling rests on the assertion that the Hybrid EC axiomatization (functional fluents plus time-to-abstract-steps mapping) preserves the trajectories of standard Event Calculus on dense time while guaranteeing termination. No equivalence theorem, model-theoretic correspondence, or bisimulation argument is supplied; validation is limited to examples. This is load-bearing for the accuracy claim.

    Authors: We agree that a formal equivalence theorem, model-theoretic correspondence, or bisimulation argument would strengthen the central accuracy claim. The manuscript presents Hybrid EC as a practical extension of DEC that incorporates functional fluents (to represent values via linear constraints) and a mapping from time to abstract steps (to support dense domains). This design is implemented directly in clingcon and clingo-lpx, with termination guaranteed by the underlying hybrid solvers whenever solutions exist. Validation is performed via examples that demonstrate accurate continuous-change modeling over rationals without discretization. While the axiomatization is constructed to extend DEC in a manner that preserves intended trajectories under the constraint semantics, the paper does not supply a formal proof of equivalence to standard EC on dense time. We will revise the manuscript to include a clearer informal explanation of the design choices and their intended semantic alignment, along with an explicit statement that the accuracy claims rest on empirical validation rather than a formal theorem. revision: partial

standing simulated objections not resolved
  • Establishing a formal equivalence theorem, model-theoretic correspondence, or bisimulation argument between the Hybrid EC axiomatization and standard Event Calculus on dense time

Circularity Check

0 steps flagged

No significant circularity; derivation relies on external solvers and example validation

full rationale

The paper introduces Hybrid EC via functional fluents and time-to-abstract-steps mapping, then implements it in external Hybrid ASP solvers (clingcon, clingo-lpx) whose behavior is treated as given. Validation occurs on examples, with claims of semantics preservation and termination not reducing to self-referential definitions, fitted inputs renamed as predictions, or load-bearing self-citations. The central claim does not collapse by construction to its inputs; the work is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach depends on the unproven semantic preservation of the time-to-abstract-steps mapping and on the termination and correctness guarantees of the external Hybrid ASP solvers; no free parameters or new invented entities are described.

axioms (1)
  • domain assumption Mapping time to abstract steps together with functional fluents preserves continuous-change semantics of Event Calculus
    Invoked to avoid discretization while retaining termination; location implied in the description of the extended axiomatization.

pith-pipeline@v0.9.1-grok · 5800 in / 1150 out tokens · 28766 ms · 2026-06-28T03:44:17.694990+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

176 extracted references · 20 canonical work pages

  1. [1]

    ECAI Workshop on Value Engineering in AI (VALE'24) , pages=

    Opportunities and Challenges of the Use of Forgetting in Symbolic XAI , author=. ECAI Workshop on Value Engineering in AI (VALE'24) , pages=. 2024 , organization=

  2. [2]

    Artificial Intelligence and Law , volume = 32, number = 4, pages =

    Joaqu. Artificial Intelligence and Law , volume = 32, number = 4, pages =

  3. [3]

    International Symposium on Computers in Education, SIIE'23 , publisher =

    Joaqu. International Symposium on Computers in Education, SIIE'23 , publisher =

  4. [4]

    Workshop of the 38th ICLP'22 , publisher =

    Joaqu. Workshop of the 38th ICLP'22 , publisher =

  5. [5]

    doi:10.20868/UPM.thesis.58189 , school =

    Joaqu. doi:10.20868/UPM.thesis.58189 , school =

  6. [6]

    Arias , year = 2016, month =

    J. Arias , year = 2016, month =

  7. [7]

    International Conference on Practical Applications of Agents and Multi-Agent Systems (PAAMS'24) , pages=

    Private-safe (logic-based) decision systems for energy assignment in agricultural cooperatives , author=. International Conference on Practical Applications of Agents and Multi-Agent Systems (PAAMS'24) , pages=. 2024 , organization=

  8. [8]

    and Arias, Joaqu

    Fidilio-Allende, Luciana. and Arias, Joaqu

  9. [9]

    20th European Conference on Multi-Agent Systems, EUMAS'23 , publisher =

    Andr. 20th European Conference on Multi-Agent Systems, EUMAS'23 , publisher =

  10. [10]

    Marin Lujak and Alberto Fern

  11. [11]

    Ondřej Vašíček and Joaquin Arias and Jan Fiedor and Gopal Gupta and Brendan Hall and Bohuslav Křena and Brian Larson and Tomáš Vojnar , year = 2025, booktitle =

  12. [12]

    Anitha Murugesan and Isaac Wong and Joaquín Arias and Robert Stroud and Srivatsan Varadarajan and Elmer Salazar and Gopal Gupta and Robin Bloomfield and John Rushby , year = 2024, journal =

  13. [13]

    Ondřej Vašíček and Joaquin Arias and Jan Fiedor and Gopal Gupta and Brendan Hall and Bohuslav Křena and Brian Larson and Sarat Chandra Varanasi and Tomáš Vojnar , year = 2024, journal =

  14. [14]

    Yankai Zeng and Abhiramon Rajashekharan and Kinjal Basu and Huaduo Wang and Joaquín Arias and Gopal Gupta , year = 2024, journal =

  15. [15]

    Gopal Gupta and Elmer Salazar and Joaqu

  16. [16]

    Sopam Dasgupta and Farhad Shakerin and Elmer Salazar and Joaqu

  17. [17]

    Yankai Zeng and Abhiramon Rajasekharan and Kinjal Basu and Huaduo Wang and Joaqu

  18. [18]

    Yankai Zeng and Abhiramon Rajasekharan and Parth Padalkar and Kinjal Basu and Joaqu

  19. [19]

    Stroud and Kateryna Netkachova and Isaac Hong Wong and Joaqu

    Srivatsan Varadarajan and Robin Bloomfield and John Rushby and Gopal Gupta and Anitha Murugesan and Robert J. Stroud and Kateryna Netkachova and Isaac Hong Wong and Joaqu. Workshops of the 43rd SAFECOMP'24 , publisher =

  20. [20]

    Stroud and Joaqu

    Anitha Murugesan and Isaac Hong Wong and Robert J. Stroud and Joaqu

  21. [21]

    Zesheng Xu and Joaqu

  22. [22]

    Prolog: The Next 50 Years , publisher =

    Gopal Gupta and Elmer Salazar and Farhad Shakerin and Joaqu. Prolog: The Next 50 Years , publisher =

  23. [23]

    Kinjal Basu and Elmer Salazar and Huaduo Wang and Joaqu

  24. [24]

    Gopal Gupta and Elmer Salazar and Sarat Chandra Varanasi and Kinjal Basu and Joaqu

  25. [25]

    Sarat Chandra Varanasi and Neda Saeedloei and Elmer Salazar and Joaqu

  26. [26]

    Sarat Chandra Varanasi and Joaqu

  27. [27]

    Basu, Kinjal and Varanasi, Sarat and Shakerin, Farhad and Arias, Joaquin and Gupta, Gopal , year = 2021, journal =

  28. [28]

    Gopal Gupta and Sarat Varnasi and Kinjal Basu and Zhuo Chen and Elmer Salazar and Farhad Shakerin and Serdar Erbatur and Fang Li and Huaduo Wang and Joaqu

  29. [29]

    Sarat Chandra Varanasi and Brendan Hall and Joaqu

  30. [30]

    Jan Wielemaker and Joaqu

  31. [31]

    8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS'21 , series =

    Brendan Hall and Sarat Chandra Varanasi and Jan Fiedor and Joaqu. 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS'21 , series =

  32. [32]

    Farhad Shakerin and Gopal Gupta , title =

  33. [33]

    2022 , publisher=

    Wang, Huaduo and Shakerin, Farhad and Gupta, Gopal , journal=. 2022 , publisher=

  34. [34]

    2022 , organization=

    Wang, Huaduo and Gupta, Gopal , booktitle=. 2022 , organization=

  35. [35]

    2024 , organization=

    Wang, Huaduo and Gupta, Gopal , booktitle=. 2024 , organization=

  36. [36]

    5th International Conference on Logic Programming , pages =

    Michael Gelfond and Vladimir Lifschitz , title =. 5th International Conference on Logic Programming , pages =

  37. [37]

    Kinjal Basu and Huaduo Wang and Nancy Dominguez and Xiangci Li and Fang Li and Sarat Chandra Varanasi and Gopal Gupta , title =

  38. [38]

    2016 , doi=

    Zhuo Chen and Kyle Marple and Elmer Salazar and Gopal Gupta and Lakshman Tamil , journal=. 2016 , doi=

  39. [39]

    Relevant Counterfactuals , booktitle =

    Lu. Relevant Counterfactuals , booktitle =. 1989 , doi =

  40. [40]

    Jason Morris , title =

  41. [41]

    2023 , month =

    Robert Kowalski and Jacinto Dávila Quintero and Galileo Sartor and Miguel Calejo , title =. 2023 , month =

  42. [42]

    2023 , doi =

    Abhiramon Rajasekharan and Yankai Zeng and Parth Padalkar and Gopal Gupta , title =. 2023 , doi =

  43. [43]

    Steve Moyle and Nicholas Allott and John Manslow , booktitle =

  44. [44]

    , publisher =

    , title =. , publisher =

  45. [45]

    , publisher =

    , title =. , publisher =. , pages =

  46. [46]

    New Generation Computing , publisher =

    Robert Kowalski and Marek Sergot , title =. New Generation Computing , publisher =. 1986 , pages =

  47. [47]

    Lee, Joohyung and Palla, Ravi , journal=

  48. [48]

    Joohyung Lee and Ravi Palla , title =

  49. [49]

    xxx , publisher =

    xxx , title =. xxx , publisher =

  50. [50]

    TPLP , volume =

    Tomi Janhunen and Roland Kaminski and Max Ostrowski and Sebastian Schellhorn and Philipp Wanko and Torsten Schaub , title =. TPLP , volume =. 2017 , doi =

  51. [51]

    Mueller , title =

    Erik T. Mueller , title =. Journal of Logic and Computation , volume =. 2004 , issn =

  52. [52]

    Sergot and Georgios Paliouras , title =

    Alexander Artikis and Marek J. Sergot and Georgios Paliouras , title =. 2015 , doi =

  53. [53]

    Processes and continuous change in a SAT-based planner , journal =

    Ji. Processes and continuous change in a SAT-based planner , journal =. 2005 , doi =

  54. [54]

    Potassco User Guide

    Martin Gebser and Roland Kaminski and Benjamin Kaufmann and Marius Lindauer and Max Ostrowski and Javier Romero and Torsten Schaub and Sven Thiele. Potassco User Guide

  55. [55]

    Abstract G ringo

    Martin Gebser and Amelia Harrison and Roland Kaminski and Vladimir Lifschitz and Torsten Schaub. Abstract G ringo. Theory and Practice of Logic Programming

  56. [56]

    Clingcon: The Next Generation

    Mutsunori Banbara and Benjamin Kaufmann and Max Ostrowski and Torsten Schaub. Clingcon: The Next Generation. Theory and Practice of Logic Programming

  57. [57]

    15th Annual NDIA Systems Engineering Conference , publisher =

    Don Ward , title =. 15th Annual NDIA Systems Engineering Conference , publisher =. 2012 , url =

  58. [59]

    Automating Semantic Analysis of System Assurance Cases Using Goal-Directed

    Anitha Murugesan and Isaac Hong Wong and Joaqu. Automating Semantic Analysis of System Assurance Cases Using Goal-Directed. Theory and Practice of Logic Programming , volume =. 2024 , url =. doi:10.1017/S1471068424000425 , timestamp =

  59. [60]

    Dill , title =

    Rajeev Alur and David L. Dill , title =. TCS , year =

  60. [61]

    Efficient Detection of Zeno Runs in Timed Automata , booktitle =

    Rodolfo G. Efficient Detection of Zeno Runs in Timed Automata , booktitle =. 2007 , url =. doi:10.1007/978-3-540-75454-1\_15 , timestamp =

  61. [62]

    Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics

    Rinast, Jonas and Schupp, Sibylle. Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics. Formal Modeling and Analysis of Timed Systems. 2012

  62. [63]

    Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics

    Rinast, Jonas and Schupp, Sibylle. Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics. FORMATS. 2012

  63. [64]

    2013 , month =

    Coarse abstractions make Zeno behaviours difficult to detect , author =. 2013 , month =. doi:10.2168/LMCS-9(1:6)2013 , journal =

  64. [65]

    Henzinger , title =

    Thomas A. Henzinger , title =. LICS , pages =. 1996 , url =. doi:10.1109/LICS.1996.561342 , timestamp =

  65. [66]

    Lamperski and Aaron D

    Andrew G. Lamperski and Aaron D. Ames , title =. 2013 , url =. doi:10.1109/TAC.2012.2208292 , timestamp =

  66. [68]

    Zhang, Jun and Johansson, Karl Henrik and et. al. , title =. IJRNC , volume =. doi:https://doi.org/10.1002/rnc.592 , url =. https://onlinelibrary.wiley.com/doi/pdf/10.1002/rnc.592 , year =

  67. [69]

    Systems & control letters , volume=

    On the regularization of Zeno hybrid automata , author=. Systems & control letters , volume=. 1999 , publisher=

  68. [70]

    Henzinger , title =

    Rajeev Alur and Thomas A. Henzinger , title =. 1997 , url =. doi:10.1007/3-540-63141-0\_6 , timestamp =

  69. [71]

    Ondřej Vašíček and Joaquin Arias and Jan Fiedor and et. al. , title =

  70. [72]

    Ondřej Vašíček and Joaquin Arias and Jan Fiedor and Gopal Gupta and Brendal Hall and Bohuslav Křena and Brian Larson and Tomáš Vojnar , title =

  71. [75]

    Theory and Practice of Logic Programming , volume =

    Ondřej Vašíček and Joaquin Arias and Jan Fiedor and Gopal Gupta and Brendan Hall and Bohuslav Křena and Brian Larson and Sarat Chandra Varanasi and Tomáš Vojnar , title =. Theory and Practice of Logic Programming , volume =. 2024 , url =. doi:10.1017/S1471068424000280 , timestamp =

  72. [76]

    ECAI , pages =

    Murray Shanahan , title =. ECAI , pages =. 1996 , timestamp =

  73. [77]

    12th European Conference on Artificial Intelligence, Budapest, Hungary, August 11-16, 1996, Proceedings , pages =

    Murray Shanahan , title =. 12th European Conference on Artificial Intelligence, Budapest, Hungary, August 11-16, 1996, Proceedings , pages =. 1996 , timestamp =

  74. [78]

    1997 , isbn =

    Murray Shanahan , title =. 1997 , isbn =

  75. [79]

    Software: Practice and Experience , volume =

    Hai-Feng Guo and Gopal Gupta , title =. Software: Practice and Experience , volume =. 2008 , pages =. doi:https://doi.org/10.1002/spe.824 , publisher=

  76. [80]

    Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP

    Joaqu. Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP. Proc. of PADL'19 -- 21st International Symposium on Practical Aspects of Declarative Languages. 2019 , pages =. doi:10.1007/978-3-030-05998-9_7 , butype =

  77. [81]

    Michael Gelfond and Vladimir Lifschitz , title =. Proc. of 5th International Conference on Logic Programming , pages =

  78. [83]

    Hatcliff, John and Larson, Brian and Carpenter, Todd and et. al. , title =. 2019 , publisher =. doi:10.1145/3357495.3357496 , journal =

  79. [84]

    Hatcliff, John and Larson, Brian , title =. 2018

  80. [85]

    Hatcliff, John and Larson, Brian , title =

Showing first 80 references.