About
SLEECVAL enables specification and validation of non-functional rules with the focus on SLEEC (social, legal, ethical, empathetic, and cultural) principles for autonomous agents. To best of our knowledge, our language and tool are novel in their support to formalise and validate normative rules that address SLEEC concerns. Our vision is to provide an automated framework to specify, validate, and verify that agents follow rules, reporting redundancy and conflicts.
SLEEC Language Syntax
SLEEC syntax is composed of defBlock and ruleBock. Definitions are recursively defined in the SLEEC language through events, measures or constants. Every event and measure have an eventID and measureID respectively. The ruleBlock consist of triggers, responses, and defeaters. A trigger can combine events as well as measures and expressions of them with any logical operation. Responses can be timed, and one can define deadlines and timeouts with responses through within construct. SLEECVAL currently handles seconds, hours and days as time units in the language . In order to handle the situations where the response event cannot happen within a required time unit, we include the otherwise construct to order the events. The concept of defeaters are conducted with unless together with a condition.
SLEEC Language Semantics into CSP
The tock-CSP processes that define the semantics of the rules are computed through a visitor pattern applied to each element of the SLEEC grammar syntax tree, with each SLEEC rule converted to a tock-CSP process. The computation is based on translation rules. Each event and measure is modelled in tock-CSP as a channel with measure types directly converted into existing CSP datatypes, or introduced as a new scalar datatype in CSP.