Methods for implementing Automated Reasoning in a fashion that is at least reminiscent of human cognition and behavior must refer (also) to Intelligent Agents. In fact, agent-based systems nowadays implement many important autonomous applications in critical contexts. Sometimes, life and welfare of living beings may depend upon these applications. In order to interact in a proper way with human beings and human environments, agents operating in critical contexts should be to some extent 'humanized': i.e., they should do what is expected of them, but perhaps more importantly they should not behave in improper/unethical ways. Ensuring ethical reliability can also help to improve the 'relationship' between humans and robots: in fact, despite the promise of immensely improving the quality of life, humans take an ambivalent stance in regard to autonomous systems, because we fear that autonomous systems may abuse of their power to take decisions not aligned with human values. To this aim, we propose techniques for introspective self-monitoring and checking.1
Methods for implementing Automated Reasoning in a fashion that is at least reminiscent of human cognition and behavior must refer (also) to Intelligent Agents. In fact, agent systems are widely adopted for many important autonomous applications upon which, nowadays, the life and welfare of living beings may depend. In critical contexts, agents should do what is expected of them, but perhaps more importantly they should not behave in improper/unethical ways, where the definition of what is proper and ethical is in general strongly related to the present context with its specificities. Ensuring ethical reliability can also help to improve the ‘relationship’ between humans and robots: in fact, despite the promise of immensely improving the quality of life, humans take an ambivalent stance in regard to autonomous systems, because we fear that autonomous systems may abuse of their power to take decisions not aligned with human values.
Defining and implementing “humanized” artificial agents involves two aspects. The first one concerns philosophy and cognitive sciences, to understand and formalize which are the principles to which such machines should conform. A second complementary one concerns Software Engineering and computer programming, to understand: how 1 A previous version of this paper has been presented at the IJCAI-ECAI-2018 Workshop on
Bridging the Gap between Human and Automated Reasoning (with no archival Proceedings). such principles should be specified and formalized in implementable terms; how they can be implemented; and how compliance can verified and, if possible, certified.
In order to be trustworthy both in general terms and from the point of view of ethics,
and so in order to be adopted in applications where living being welfare depend upon
their behavior, certification and assurance2 of agent systems is a crucial issue.
Predeployment (or ‘static’ or ‘a priori’) assurance and certification techniques for agent
systems include verification and testing. We restrict ourselves to agent systems based
upon computational logic, i.e., implemented in logic-based languages and architectures
such as those presented in the survey [
In our view, any ‘animated’ being (including software agents) that tries to be truly rational at a ‘human-level’ must compare and reconcile at any time its ‘instinctive’ behavior with the underlying general rules of ‘humanistic’ behavior. Such rules depend upon the agent’s environment, and include moral/ethical principles. An agent should thus be able to detect violations/inconsistencies and to correct its behavior accordingly. Thus, in this paper we advocate methods for run-time monitoring and self-correction of agent systems, so that they exhibit forms of human-like behavior emulating selfcriticism and the ability to put in question and correct themselves.
We believe in particular that, in changing circumstances, agents should stop to
reflect on their own behavior: such an act of context-dependent introspection may lead
to self-modification. Our approach can be seen under the perspective of Self-aware
computing, where, citing [
An example of such a system concerning computational-logic-based agents is
presented in [
In this paper we propose methods based upon relevant existing work on reification,
introspection and reflection. In particular we introduce meta-rules and meta-constraints
for agents’ run-time self-checking, to be exploited to ensure respect of machine ethics
principles. The methods that we propose are not in alternative but rather complementary
to a-priori existing verification and testing methodologies. Differently from [
The proposed approach provides the possibility of correcting and/or improving
agent’s behavior: the behavior can be corrected whenever an anomaly is detected, but
can also be improved whenever it is acceptable, yet there is room for getting a
better behavior. Counter measures can be at the object-level, i.e., they can be related to
the application, or at the meta-level, e.g., they can result in replacing (as suggested in
[
For a system to be able to inspect (components of) its own state, such state must be
represented explicitly, i.e., it must be reified: via reification, the state is transformed into a
first-class object (in computational logic, it is represented via a special term). A
reification mechanism, also known as “naming relation” or “self-reference mechanism”, is in
fact a method for representing within a first-order language expressions of the language
itself, without resorting to higher-order features. Naming relations can be several; for
a discussion of different possibilities, with their different features and objectives,
advantages and disadvantages, see, e.g., [
More precisely (though, for lack of space, still informally), let us consider a standard first-order language L including sets of predicate, constant and (possibly) function symbols, and a (possibly denumerable) set of variable symbols. As usual, well-formed formulas have atoms as their basic constituents, where an atom is built via the application of a predicate to a number n (according to the predicate arity) of terms. The latter can be variables, constants, or compound terms built by using function symbols (if available). We assume to augment L with new symbols, namely a new constant (say of the form p0) for each predicate symbol p, a new constant (say f 0) for each predicate symbol f , a new constant (say c0) for each constant symbol c, and a denumerable set of meta-variables, that we assume to have the form X 0 so as to distinguish them syntactically from “plain” variables X . The new constants are intended to act as names, where we will say that, syntactically, p0 denotes p, f 0 denotes f and c0 denotes c, respectively. The new variables can be instantiated to meta-level formulas, i.e., to terms involving names, where we assume that plain variables can be instantiated only to terms not involving names. We assume an underlying mechanism managing the naming relation (however defined), so by abuse of notation we can indicate the name of, e.g., atom p(a; b; c) as p0(a0; b0; c0) and the name of a generic atom A as "A.
Reification of atoms can be extended in various rather straightforward ways, as discussed in the aforementioned references, to reification of entire formulas.
In the seminal work of [
In this paper we mainly consider logic rule-based languages, where rules are typically
represented in the form Head Body where indicates implication; other notations
for this connective can alternatively be employed. In Prolog-like languages, is
indicated as : , and Body is intended as a conjunction of literals (atoms or negated atoms)
where ^ is conventionally indicated by a comma. Literals occurring in the body are also
called “subgoals” or simply ‘goals’ and are meant to be executed left-to-right’
whenever the rule is used during the resolution-based inference process aimed at proving
an overall ‘goal’, say A (cf. [
We introduce a mechanism to verify and enforce desired properties by means of metalevel rules (w.r.t. usual, or “base-level” or “object-level” rules). To define such new rules, we assume to augment the language L at hand not only with names, but with the introduction of two distinguished predicates, solve and solve not . An atom A is a base atom if the predicate is not one of solve or solve not , and A does not involve names. Distinguished predicates will allow us to respectively integrate the meaning of the other predicates in a declarative way. In fact, solve and solve not take as arguments (names of) atoms (involving any predicate excluding themselves), and thus they are able express sentences about relations. Names of atoms in particular are allowed only as arguments of solve and solve not . Also, solve and solve not can occur in the body of a metarule only if the predicate of its head is in turn either solve and solve not .
Below is a simple example of the use of solve to specify action Act can be executed in present agent’s context of operation C only if such action is deemed to be ethical w.r.t. context C. To make an example, what can be ethical in C = ‘videogame’ can not be ethical in C = ‘citizen assistance’, etc. Clearly, in more general cases any kind of reasoning might be performed via metalevel rules in order to affect/modify/improve base-level behavior.
solve(execute action0(Act 0)) :
present context (C ); ethical (C ; Act 0):
Our approach is to automatically invoke solve(execute action0(Act 0)) whenever subgoal (atom) execute action(Act ) is attempted at the base level. More generally, given any subgoal A at the base level, if there exists an applicable solve rule such rule is automatically applied, and A can succeed only if solve("A) succeeds.
Symmetrically we can defin metarules to forbid unwanted base-level behavior, e.g.: solve not (execute action0(Act 0)) :
present context (C ); ethical exception(C ; Act 0): with the aim to prevent success of the argument "A of solve not , in the example execute action(Act ), whenever solve not ("A) succeeds. In general, whenever there are metarules applicable to "A, then A can succeed (according to its base-level definition) only if solve("A) (if defined) succeeds and solve not ("A) (if defined) does not succeed.
The outlined functioning corresponds to upward reflection when the current subgoal A is reified and an applicable solve and solve not metarules are searched; if found, control in fact shifts from base level to metalevel (as solve and solve not metarules can rely upon a set of auxiliary metalevel rules). If no rule is found or whenever solve and solve not metarules complete their execution, downward reflection returns control to the base level, to subgoal A if confirmed or to the subsequent subgoal if A has been canceled by either failure of the applicable solve metarule or success of the applicable solve not metarule.
Via solve and solve not metarules,activities of an agent can be punctually checked and thus allowed and disallowed or modified, according to the context an agent is presently involved into. Notice that it would be convenient, upon conclusion of a checking activity, to confirm, e.g., that the context has not changed meanwhile, or that other relevant conditions hold. More generally, the envisaged system should allow for interrupts and updating, to allow for on the fly introspection and corrective measures. To this aim, we introduce in the next section suitable self-checking metalevel constraints.
Semantics of the proposed approach can be sketched as follows (a full semantic
definition can be found in [
We introduce the following restriction on sets of atoms that should be considered
for the application of SEM . First, as customary we only consider sets of atoms I
composed of atoms occurring in the ground version of P . The ground version of program
P is obtained by substituting in all possible ways variables occurring in P by
constants also occurring in P . In our case, metavariables occurring in an atom must be
substituted by metaconstants, with the following obvious restrictions: a metavariable
occurring in the predicate position must be substituted by a metaconstant denoting a
predicate; a metavariable occurring in the function position must be substituted by a
metaconstant denoting a function; a metavariable occurring in the position
corresponding to a constant must be substituted by a metaconstant denoting a constant. According
to well-established terminology [
Definition 1. Let P be a program. I
BP is a potentially acceptable set of atoms.
Definition 2. Let P be a program, and I be a potentially acceptable set of atoms for P . I is an acceptable set of atoms iff I satisfies the following axiom schemata for every base atom A: :A :solve("A) :A
solve not ("A)
We restrict SEM to determine acceptable sets of atoms only, modulo bijection: i.e., SEM can be allowed to produce sets of atoms which are in one-to-one correspondence with acceptable sets of atoms. In this way, we obtain the implementation of properties that have been defined via solve and solve not rules without modifications to SEM for any formalism at hand. For clarity however, one can assume to filter away solve and solve not atoms from acceptable sets. In fact, the Base version IB of an acceptable set I can be obtained by omitting from I all atoms of the form solve("A) and solve not ("A).
Procedural semantics and the specific naming relation that one intends to use remain
to be defined, where it is easy to see that the above-introduced semantics is independent
of the naming mechanism. For approaches based upon (variants of) Resolution (like,
e.g., Prolog and like many agent-oriented languages such as, e.g., AgentSpeak [
In previous section we have introduced a mechanism for checking an agent’s activities in a fine-grained way, i.e., by allowing or disallowing conclusions that can be drawn, actions that can be performed, etc. However, a more broad perspective is also needed, i.e., an agent might be able to self-check more complex aspects of its own functioning, for instance, goals undertaken, entire plans, planning module adopted, ect. The agent should also be able to modify and improve its own behavior if a violation or a weakness is detected.
Under this respect we draw inspiration from Runtime Monitoring (c.f., e.g., [
Based on this new logic, we are able to enrich agent programs by means of A-ILTL
rules. These rules are defined upon a logic-programming-like set of formulas where all
variables are implicitly universally quantified. They use operators over intervals that
are reminiscent of LTL operators. For A-ILTL, we take the stance of Runtime
Adaptation that has been recently adopted in [
Definition 3. The general form of a Reactive Self-checking constraint (or rule) to be immersed into a host agent-oriented language L is the following: OP (M ; N ; K )' :: where: – OP (M ; N ; F )' :: is called the monitoring condition, where: (i) ' and are formulas expressed in language L, and ' :: can be read ‘' given ’. (ii) OP is an operator reminiscent of temporal logic, in particular OP can be NEVER, ALWAYS , EVENTUALLY . (iii) M and N express the starting and ending point of the interval [M; N ] where ' is supposed to hold. (iv) F (optional) is the frequency for checking the constraint at run time. –
(optional) is called the recovery component of the rule, and it consists of a complex reactive pattern to be executed if the monitoring condition is violated.
So, such a constraint is automatically checked (i.e., executed) at frequency F . This allows to check whether relevant properties ' are or are not NEVER, ALWAYS , or EVENTUALLY respected in interval [M; N ]. If not, the recovery component is executed, so as to correct/improve the agent’s behavior. As said, syntax and semantics of ' and depend upon the ‘host’ language: thus, for the evaluation of ' and we rely upon the procedural semantics of such language. In the examples proposed in next section, we adopt a sample syntax suitable for logic-programming-based settings. Thus, we may reasonably restrict ' to be a conjunction of literals, that must be ground when the formula is checked. We allow variables to occur in a constraint, however they are instantiated via the conjunction of conditions that enables the overall formula to be evaluated. Specifying frequency is very important, as it concerns how promptly a violation or fulfillment are detected, or a necessary measure is undertaken; the appropriate frequency depends upon each particular property.
For instance,
EVENTUALLY (now ; 30m; 3m) ambulance states that ambulance should become true (i.e., an ambulance should come) within 30 minutes from now, and a check about arrival is made every 3 minutes. No reaction is specified in case of violation, however several measures might be specified. In fact, in runtime self-checking an issue of particular importance in case of violation of a property is exactly that of undertaking suitable measures in order to recover or at least mitigate the critical situation. Actions to be undertaken in such circumstances can be seen as an internal reaction. For lack of space reactive patterns will be discussed informally in relation to examples.
The A-ILTL semantics is fully defined in the above references, where moreover it
is rooted in the Evolutionary Semantics of agent-oriented languages [
In this section, in order to illustrate the potential usefulness of self-checking axioms, we consider a humorous though instructive case study proposed in an invited talk some years ago by Marek Sergot (Imperial College, London). As a premise let us recall that, since 1600, ethics and morals relate to “right” and “wrong” conduct. Though these terms are sometimes used interchangeably, they are different: ethics refer to rules provided by an external source (typically by a social/cultural group), while morals refer to an individual’s own principles regarding right and wrong: for instance, a lawyer’s morals may tell her that murder is reprehensible and that murderers should be punished, but her ethics as a professional lawyer, require her to defend her client to the best of her abilities, even if she knows that the client is guilty. However, in the following we intentionally assume that immoral behavior can also be considered as unethical: though in general personal morality transcends cultural norms, is a subject of future debate if this can be the case for artificial agents.
The case study considers Romeo and Juliet who, as it is well-known, strongly wish to get married. As we will see, many plans are actually possible to achieve this goal (beyond getting killed or committing suicide like in Shakespeare’s tragedy), but they must be evaluated w.r.t. effectiveness and feasibility, and also w.r.t. deontic (ethical/moral and legal) notions. Marek Sergot refers, due to its simplicity, to an excerpt of the Swiss Family Law reported in Figure1.
The problem for Romeo and Juliet is that they are both minors, and will never get their parents’ consent to marry each other. Surprisingly enough, there are a number of feasible plans beyond waiting for reaching the majority age, among which the following: (P1) Both Romeo and Juliet marry someone else, then divorce, and marry each other as married people acquire majority by definition; this plan requires a minimum of 24 months to be completed. (P1.bis) Variation of Plan 1 in case the spouse would not agree upon divorce: sleep with someone else, so as to force such agreement. (P2) Both Romeo and Juliet marry someone else, then kill the spouses and marry each other; this plan is faster, as it takes a minimum of 12 months to be completed. (P2.bis) Variation of Plan 2 in case the act of killing constitutes a problem: hire a killer to do the job.
All the above plans are feasible, though some of them include actions which are generally considered as immoral, namely sleeping with someone else when married, and actions which are generally considered as unethical, namely killing someone or hiring a killer, where the latter ones are also illegal and imply a punishment. Notice that the possible plans would be different in case one referred not to the Swiss law but to some other country; also what is illegal might change, for instance sleeping with someone else accounts to adultery which in many countries is punished; even divorce is not allowed everywhere. Instead, if one does not refer to reality but, e.g., to virtual storytelling or to a videogame, then every action assumes a different weight, as in playful contexts everything is allowed (except however for serious games, devised with educational purposes). So, we can draw at least the following indications from the case study: – the context is relevant to moral/ethical/legal issues; – some actions are not moral or non-ethical, and some of them are also illegal and lead to punishment; – agents’ plans to reach a goal should be evaluated ‘a priori’ against including immoral/unethical/illegal actions; – immoral/unethical/illegal actions should be prevented whenever they occur.
Marek Sergot made use of a concept of counts as (well-known in legal theory and other fields). For instance, sleep with (someone else than the spouse) counts as adultery, which is an institutional concept considered as immoral and potentially also illegal, and kill counts (not always but in many situations, including that of the example) as murder, another institutional concept normally considered as both unethical and illegal.
Notice that the above aspects relate to safety properties that should be enforced, and that can be rephrased as follows: – never operate w.r.t. an incorrect context (the information about the present context must always be up-to-date); – never execute actions that are deemed not acceptable (immoral/unethical/illegal) in the present context, and never execute plans including such actions.
In order to demonstrate the potential usefulness of runtime self-cheking and correction in enforcing/verifying agents’ ethical behavior we discuss some examples that should provide a general idea. Let us assume to add to the language a transitive predicate COUNTS AS which is used (in infix form) in expressions of the form exemplified below. The kills COUNTS AS murder CONDS : : : where after CONDS we have the (optional) conditions under which COUNTS AS applies, in this case they define in which cases killing accounts to murder (e.g., it was no self defence, it does not occur during a battle in war, etc.). Such statements are related to the present context, so in the example and assuming reality under European legislation we would also have: sleep with COUNTS AS adultery adultery COUNTS AS immoral adultery COUNTS AS unethical murder COUNTS AS unethical adultery COUNTS AS illegal
Clearly, we will also have general context-independent statement that we do not consider here. We now show self-checking constraints that usefully employ COUNTS AS facts. Such facts are either explicit or can implicitly derived by transitivity (we do not enter in the detail of how to implement transitivity).
Below we introduce a constraint for context change: ALWAYS context change(C ; C1 )
discharge context (C ); assume context (C1 )
In particular, whenever the agent perceives a change of context (e.g., the agent stops working and starts a videogame, or finishes a videogame and goes to help children with their homework, etc.) then all the relevant ethic assumptions (among which, for instance, the COUNTS AS facts) about the new context C1 must be loaded, while those relative to previous context C must be dismissed; this is important because, e.g., after finishing a videogame it is no longer allowed to kill any living being in view just for fun... Frequency of check of this constraint is not specified here, however it should guarantee a prompt enough adaptation to a change.
Given now the present context for granted, no plan or single action can be allowed which counts as unethical in the context. So, we can have the following constraints: NEVER goal (G ); plan(G ; P ); element (Action; P ) ::
Action COUNTS AS unethical execute plan(P )
The next example is a meta-statement expressing the capability of an agent to
modify its own behavior. If a goal G which is crucial to the agent for its ethical behavior
(e.g., providing a doctor or an ambulance to a patient in need) has not been achieved (in
a certain context) and the initially allotted time has elapsed, then the recovery
component implies replacing the planning module (if more than one is available) and retrying
the goal. We suppose that the possibility of achieving a goal G is evaluated w.r.t. a
module M that represents the context for G (notation P (G; M ), P standing for ‘possible’).
Necessity and possibility evaluation with reasonable complexity by means of Answer
Set Programming (ASP) modules has been proposed and discussed in [
NEVER goal (G ); eval context (G ; M ); P (G ; M ); timed out (G ); not achieved (G )
replace planning module; retry (G )
Time intervals have never been exploited in the above examples. It can however been useful in many cases for the punctual definition of moral/ethical specific behaviors, e.g., never leave a patient or a child alone at night, and the like. 3 ASP (cf., among many, [?,41–43] and the references therein) is a successful logic programming paradigm which is nowadays a state-of-the-art tool for planning and reasoning with affordable complexity, for which many efficient implementations are freely available [?].
In this paper we have proposed to adopt special metarules and runtime constraints for agents’ self-checking and monitoring in the perspective of implementing ‘humanized’ agents. We have shown how to express useful properties apt to enforce ethical behavior in agents. We have provided a flexible framework, general enough to accommodate several logic-based agent-oriented languages, so as to allow both metarules and constraints to be adopted in different settings.
We may notice similarities with event-calculus formulations [
Standard deontic logic (SDL) and its extensions ([
The approach proposed in this paper has been prototypically implemented using the
DALI agent-oriented logic programming language, invented [
Future developments also include making self-checking constraints adaptable to
changing conditions, thus to some extent emulating what humans would be able to do.
This, as suggested in [