Jan Fiedor

Ondřej Vašíček, Joaquín Arias, Jan Fiedor et al.

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.

Brendan Hall, Sarat Chandra Varanasi, Jan Fiedor et al.

We consider requirements for cyber-physical systems represented in constrained natural language. We present novel automated techniques for aiding in the development of these requirements so that they are consistent and can withstand perceived failures. We show how cyber-physical systems' requirements can be modeled using the event calculus (EC), a formalism used in AI for representing actions and change. We also show how answer set programming (ASP) and its query-driven implementation s(CASP) can be used to directly realize the event calculus model of the requirements. This event calculus model can be used to automatically validate the requirements. Since ASP is an expressive knowledge representation language, it can also be used to represent contextual knowledge about cyber-physical systems, which, in turn, can be used to find gaps in their requirements specifications. We illustrate our approach through an altitude alerting system from the avionics domain.