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 they implement many important autonomous applications upon which, nowadays, the life and welfare of living beings may depend. In such contexts, 'humanized' agents should do what is expected of them, but perhaps more importantly they should not behave in improper/unethical ways given the present context. We propose techniques for introspective selfmonitoring and checking.
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 such contexts, agents should do what is expected of them, but perhaps more importantly they should not behave in improper/unethical ways given the present context.
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 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 assurance1 of agent systems is a
crucial issue. Pre-deployment (or ’static’ or ’a priori’) assurance
1Assurance can be defined as “the level of confidence that
software is free from vulnerabilities, either intentionally designed into
the software or accidentally inserted at any time during its lifecycle,
and that the software functions in the intended manner” is related
to dependability, i.e., to ensuring (or at least obtaining a reasonable
and certification techniques for agent systems include
verification and testing. We restrict ourselves to agent systems
based upon computational logic, i.e., implemented in
logicbased languages and architectures such as those presented in
the survey [Bordini et al., 2006]. Most verification methods
for logical agents rely upon model-checking
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 runtime 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 selfmodification. Our approach can be seen under the perspective of Self-aware computing, where, citing [Tørresen et al., 2015], Self-aware and self-expressive computing describes an emerging paradigm for systems and applications that proactively gather information; maintain knowledge about their own internal states and environments; and then use this knowledge to reason about behaviors, revise self-imposed goals, and self-adapt.: : : Systems that gather unpredictable input data while responding and self-adapting in uncertain environments are transforming our relationship with and use of computers. As argued in [Amir et al., 2007], From an autonomous agent view, a self-aware system must have sensors, effectors, memory (including representation of state), conflict detection and handling, reasoning, learning, goal setting, and an explicit awareness of any assumptions. The system should be reactive, deliberative, and reflective.
An example of such a system concerning computationallogic-based agents is presented in [Anderson and Perlis, 2005], which defines a time-based active logic and a confidence) that system designers and users can rely upon the system.
Metacognitive Loop (MCL), that involves a system monitoring, reasoning and meta-reasoning about and if necessary altering its own behavior. As discussed in [Anderson and Perlis, 2005], MCL continuously monitors an agent’s expectations, notices when they are violated, assesses the cause of the violation and guides the system to an appropriate response. In the terms of [Amir et al., 2007] this is an example of Explicit Self-Awareness, where the computer system has a full-fledged self-model representing knowledge about itself.
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 [Anderson and Perlis, 2005] we do not aim to continuously monitor the entire system’s state, but rather to monitor either upon every occurrence or at suitable customizable frequency only the activities that a designer deems to be relevant for keeping the system’s behavior within a desired range. In the terms of [Amir et al., 2007] we aim to build SelfMonitoring systems that “monitor, evaluate and intervene in their internal processes, in a purposive way”.
In [Rushby, 2008], it is advocated in fact that for adaptive systems (of which agents are clearly a particularly interesting case) assurance methodologies should whenever possible imply not only detection but also recovery from software failure, due often to incomplete specifications or to unexpected changes in the system’s environment.
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
objectlevel, i.e., they can be related to the application, or at the
meta-level, e.g., they can result in replacing
Introspection and reflection have long being studied in Computational Logic, see among others [Konolige, 1988; van Harmelen et al., 1992; Perlis and Subrahmanian, 1994; Barklund et al., 2000], and the survey [Costantini, 2002]. So, in this paper we do not propose new techniques or new semantics. The application of concepts of introspection and reflection to ’Humanizing Intelligent Software Agents’ however is new, and to the best of our knowledge unprecedented in the literature. So, in our proposal techniques that have been widely applied in many fields in the past can now find a new important realm of application. We have been stimulated and to some extent influenced by the important recent book by Luis Moniz Pereira on programming Machine Ethics [Pereira and Saptawijaya, 2016]: in fact, along the paper we consider Machine Ethics topics as a testbed. The proposed techniques can in fact contribute to ’humanize’ agents under many respects, where the machine Ethics field can be considered as an interesting and very important ’drosophila’ for demonstration purposes. The paper is organized as follows. We first provide basic concepts concerning reification and introspection/reflection. Then we introduce special metarules and meta-constraints for agents’ self-checking. Then we show their usability on a case study. Finally we discuss related work and propose some concluding remarks. 2
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., [Perlis and Subrahmanian, 1994; van Harmelen, 1992; Barklund et al., 1995] where the topic is treated in a fully formal way. However, all naming mechanisms are based upon introducing distinguished constants, function symbols (if needed) and predicates, devised to construct names. For instance, gives atom p(a; b; c) a name might be atom(pred (p0); args([a0; b0; c0]) where p0 and a0; b0; c0 are new constants intended as names for the syntactic elements p and a; b; c and notice that: p is a predicate symbol (which is not a first-class object in first-order settings), atom is a distinguished predicate symbol, args a distinguished function symbol and [: : :] is a list.
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 metavariables, that we assume to have the form X0 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 [Smith, 1984] for LISP, then extended to Prolog [Dell’Acqua, 1989], an upward reflection operation determines the reification of the entire language interpreter’s state, the interruption of the interpreter’s functioning and the activation of a new instance of the interpreter on the reified state (at an “upper level”). Such state could thus be inspected and modified with the aim to improve the system’s behavior and performance; at the end, an operation of downward reflection resumed the functioning of the “lower level” interpreter on the modified state. The process might iterate over any number of levels, thus simulating an “infinite tower” of interpreters. The advantage of having the entire interpreter’s state available is however balanced by the disadvantage of such state representation being quite low-level, and so modification related to reasoning are, if not impossible, quite difficult and awkward to perform. Other approaches such as [Costantini and Lanzarone, 1989; Grosof et al., 2017] reify upon need aspects of an agent’s state. In this paper we embrace the viewpoint of the latter approaches. 3
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
We introduce a mechanism to verify and enforce desired properties by means of metalevel rules (w.r.t. usual, or “baselevel” 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
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 [Lloyd, 1987], we therefore require I BP , where BP is the Herbrand Base of P , given previously-stated limitations on variable substitution. Then, we pose some more substantial requirements. As said before, by "A we intend a name of base atom A.
Definition 1 Let P be a program. I acceptable set of atoms.
BP is a potentially 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
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
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 AILTL, we take the stance of Runtime Adaptation that has been recently adopted in [Cassar et al., 2017]: in fact, A-ILTL rules (monitors) can execute adaptation actions upon detecting incorrect behavior, rather than just indicating violations.
In a-ILTL, we can define the following meta-axioms. 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 [Costantini and Tocchio, 2005], (applicable to virtually all computational-logic-based languages). In this way, time instants correspond to states in agents’ evolution. 5
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 anyway, whenever they occur.
Marek Sergot made use of a concept of counts as (wellknown 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 selfchecking 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 has been discussed in relevant literature (omitted for anonymity). Ife the goal is still deemed to be possible but has not been achieved before a certain deadline, the reaction consists in substituting the present planning module and re-trying the goal.
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. Also, expressions that check over (partially specified) sequences of past and expected events as discussed in relevant literature (omitted for anonymity) can be potentially useful. 6
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 [Kowalski and Sergot, 1986]. In fact, recent work presented in [Berreby et al., 2017] extends the event calculus for a-priori checking of agents’ plans. [Tufis and Ganascia, 2014] treats the run-time checking of actions performed by BDI agents, and proposes an implementation under the JADE platform; this approach is related to ours, though the temporal aspects and the correction of violations are not present there.
Deontic logic has been used for building well-behaved
ethical agents, like, e.g., in the approach of [Bringsjord et al.,
2006]. However, this approach requires an expressive
deontic logic. To obtain such expressiveness, one needs highly
hybrid modal and deontic logics that are undecidable. Even
for decidable logics such as the zero-order version of Horty’s
System [Horty, 2001], decision procedures are likely to
exhibit inordinate computational complexity. In addition, their
approach is not generally applicable to agent-oriented
frameworks. There are also other challenges related to some
paradoxes and limitations of deontic logic family
Future work includes making self-checking constraints adaptable to changing conditions, thus to some extent emulating what humans would be able to do. This, as suggested in [Rushby, 2008], might be done via automated synthesis of runtime constraints. This by extracting from the history of an agent’s activity invariants expressing relevant situations. An important issue is that of devising a useful integration and synergy between declarative a-priori verification techniques such as those of [Berreby et al., 2017] with the proposed runtime self-checking. The idea of [Tufis and Ganascia, 2014] of a dynamic set of abstract and active rules will also be taken into serious consideration.