iCCalc  and  mcLUCA

Tutorial

Note: this tutorial doesn't stand alone. It will be much clearer after a reading of the defining paper on C+, Nonmonotonic Causal Theories by Giunchiglia, Lee, Lifschitz, McCain and Turner.

The example action description cornucopia contains examples of all input syntax accepted by iCCalc. If you are not sure how to write something, or what a given bit of syntax means, the answer is probably there.

The running example here concerns the letter-writing activities of the New England Transcendentalists (?). For more examples of iCCalc input syntax, see the files: library, light, monkey, rooms, russianChambers and russianND.

Running iCCalc

After installation, iCCalc can be run using the script 'iccalc'. This accepts a number of command-line options:

All additional command-line arguments are deemed to be action description source files. So, if the current working directory had an action description source file 'monkey', I could type

    % iccalc monkey

to start Prolog, compile iccalc, and then load the 'monkey' action description.

Action Description Source Files

Action descriptions of the language C+ (see the paper Nonmonotonic Causal Theories by Giunchiglia, Lee, Lifschitz, McCain and Turner) define labelled transition systems. Accordingly, the input files to iCCalc are specifications of C+ action descriptions, where the syntax is very close to C+, but with a number of convenient extra features to allowing concision in the specifications. In addition, action description source files can contain definitions of queries, questions that iCCalc can answer about runs through the transition system. (We will call the source files 'action descriptions' where this doesn't introduce confusion.)

The labelled transition systems defined by a C+ action description are graphs, whose nodes represent states of the system being modelled, and whose edges represent the possible transitions between states.

As well as supporting action descriptions of C+, iCCalc also supports action descriptions of that language's various extensions, including nC+, pC+, and their combination npC+. The syntax of the source files for these various languages is described below. Note that all of the various extensions use the common elements of source files for C+.

Action descriptions can be loaded using 'loadf( )' from within iCCalc or mcLUCA. The predicate reloadf/0 reloads a current version of whichever files are currently loaded.

Signatures

The signatures of C+ action descriptions are multi-valued and propositional, and are divided into 'fluent constants' and 'action constants'. Fluent constants are used to describe properties of objects and the environment; the values given to fluent constants determine what state the system is in. Action constants are used to represent the actions and events, and properties of them, that can occur in the system.

As an example, we will consider a domain where two agents, Emerson and Thoreau, can move between two locations, Harvard and Walden. Emerson and Thoreau can be pleased or not, and their emotional state can either be turbulent, or not. As well as moving between locations, they can write to one another. There are six fluent constants, which can be specified as follows:

    fc(loc(A)) :- agent(A).
    fc(pleased(A)) :- agent(A).
    fc(turbulent(A)) :- agent(A).
    agent(emerson).
    agent(thoreau).

Fluent constants can be Boolean or not. If they are Boolean, there is no need to declare their domain, but if they are non-Boolean, then it is necessary to say what values the constants can take. The constants 'pleased( )' and 'turbulent( )' are Boolean: an agent is either pleased or not, and turbulent or not. The constant 'loc( )' is non-Boolean, and we declare its domain thus:

    domain(loc(A), L) :- agent(A), location(L).
    location(harvard).
    location(walden).

The action constants and their domains are specified as follows:

    ac(A^move) :- agent(A).
    ac(A^writeTo^A1) :- agent(A), agent(A1), A \= A1.
    domain(A^move, L) :- agent(A), location(L).
    domain(A^move, ff) :- agent(A).

The domain declarations for 'move' mean that an agent can either move to a location, or else not move at all (stand still).

Statically-determined fluent constants are declared using facts of the predicate sdfc/1, along the same lines as fc/1, above.

The predicates agent/1 and location/1, above, are user-defined. iCCalc allows the user to use arbitrary Prolog clauses in the definitions of signatures, causal laws and queries. This increases the concision of action description source files. (Another source of concision is the use of variables: see below.)

Causal Laws

Causal laws in C+ are of three types: static, dynamic, and action. There are a number of abbreviations for commonly-used forms of the various kinds of law.

It is common to declare all or some fluent constants as inertial: the values of these fluent constants persist, by default, as the system changes. In our example action description, we have:

    inertial(FC) :- fc(FC).
    exogenous(AC) :- ac(FC).

The 'exogenous' declaration means that action constants can take on any value in a transition (unless prevented from doing so by other causal laws).
The other causal laws of the action description are:

    caused loc(A)=L after A^move=L :- agent(A), location(L).
    nonexecutable A^move=L if loc(A)=L :- agent(A), location(L).
    caused pleased(A1) after A^writeTo^A1 :- agent(A), agent(A1), A \= A1.
    caused -turbulent(A) after A^writeTo^A1 :- agent(A), agent(A1), A \= A1.

The first law states that the location of an agent is L, after the agent moves to that location. The second states that an agent cannot move to a location if he is already there. The third law states that an agent is pleased after somebody else writes to him. The fourth states that an agent is no longer turbulent after he has written to someone else.

Variables

The repeated presence of 'agent(A)' and 'location(L)' in the bodies of the clauses above can be avoided by declaring variables in the source file. These have the form

    <VARS> :: L1,...,Ln.

Where <VARS> is a number of variables separated by commas, with a 'head variable' first. For example, in our example action description we can declare:

    A,A1 :: agent(A).
    L,L1 :: location(L).

Now, whenever a variable 'A' appears elsewhere in the source file, the clause in which it appears will be partially grounded by every value of 'A' for which 'agent(A)' is true. The same will be applied to every other variable after 'A' in the list: so that if 'A1' appears in the source file, it will also be grounded to every agent.

This means, for instance, that instead of the first clause declaring the 'loc( )' fluent constant, above, we can simply write:

    fc(loc(A)).

The domain can be specified by:

    domain(loc(A), L).

The full action description for the example so far is emerson01.

User-Defined Queries

Given an action description, to query iCCalcc is to ask it to find runs through the labelled transition system defined by the action description that are consistent with information passed in the query. This information states what must be true at various points during the run.

The predicate query/3 is used to specify queries in source files. The first argument is an identifier, which can be any Prolog term, for the query. The second is the length of the runs which will be considered in solving the query. The third argument is a list specifying what must be true of the run. Here is an example:

    query(eh, 1, [0:(emerson^move)=harvard]).

This query defines the transitions (runs of length of 1) where Emerson goes to Harvard: where the action constant 'emerson^move' has the value 'harvard' at time 0. Another example:

    query(bp, 1, [-(0:pleased(emerson)),
                        -(0:pleased(thoreau)),
                        1:pleased(emerson),
                        1:pleased(thoreau)]).

This query defines transitions from states where neither is pleased, to states where both agents are pleased.

These queries could be saved in the same source file as the action description, and loaded with it, but in this example we keep them in a separate file, emerson01queries. They can be loaded, together with the action description, by typing:

    % iccalc emerson01 emerson01queries

After loading, the first query can be answered by typing at the Prolog prompt:

    ?- query eh.

This will produce as output all runs through the labelled transition system defined by the action description that are consistent with the query information.

Instead of keeping queries in the source files, they can also be posed on-the-fly using the query/2 predicate. This does the same work as query/3, but with the first argument omitted. So after loading the 'emerson01' action description, it is possible to type at the Prolog prompt:

    ?- query(1, [0:(emerson^move)=harvard]).

This then does exactly the same as 'query eh'.

The argument of query/2 and query/3 that specifies the length of run to be considered in solving the query can also denote a range, m..n, where m < n. iCCalc will then try to solve the query for runs of length m; if it fails, it will consider runs of length m+1; and so on, up to n. In that case the prefix 'max:' can be used instead of an integer to specify fluents that must be true in the final state of the run. For example:

    ?- query(2..4, [0:(loc(emerson)=harvard),
                          max:(loc(emerson)=harvard)]).

This defines runs of length 2--4 where Emerson is initially in Harvard, and is in Walden at the end of the run. Since there is such a run of length 2, iCCalc would output all runs of length 2 that satisfy the constraints, and then stop, without considering the runs of length 3 and 4.

Prolog can occur in the body of query/3 clauses. For example:

    query(x, 1, List) :- findall(0:loc(X)=harvard, agent(X), List).

Built-In Queries

There are several built-in queries:

More built-in queries are added if the action description is in nC+, as described below.

nC+

nC+ is described in the paper Agent Strands in the Action Language nC+. It is an extension of C+, used for representing and reasoning about norm-governed systems, often norm-governed agent systems. Syntactically, nC+ adds several new forms of law to C+ action description; the semantic effect of these new laws is to classify states, transitions, and agents' contributions to transitions as good or bad, licit or illicit, and so on---which we represent as a colouring of green and red. We stress: these laws do not change the structure of the labelled transition system, merely the deontic classification of its states and transitions.

To emerson01 we first add the state permission law:

    notpermitted loc(thoreau)=walden if loc(A)=walden :- A \= thoreau.

This means that if another agent is at Walden, it is bad for Thoreau to be there. State permission laws are written 'notpermitted F.', where 'F' is a conjunction of atoms, or 'notpermitted F if G', where 'F' and 'G' are conjunctions of atoms. 'F' must contain fluent constants only. Action permission laws have the same form but 'F' should contain action constants, not fluent constants.

Agent-specific permission laws are used to determine which behaviours of an agent are green or red. For agent-specific permission laws to be used, therefore, there should be a declaration of who the agents are; this is done in the source file using the predicate agent/1. Agent-specific permission laws then take the same form as action permission laws, with the name of the agent at the front. For example:

    agent(emerson).
    agent(thoreau).
    emerson notpermitted emerson^move=harvard & -(thoreau^move=harvard).
    thoreau notpermitted thoreau^writeTo^emerson if loc(thoreau)=walden.

The first agent-specific law applies to Emerson, and states that if he moves to Harvard when Thoreau isn't moving to Harvard, then Emerson is doing something wrong. The second agent-specific permission law applies to Thoreau: Thoreau is acting badly whenever he writes to Emerson from Walden.

Optionally, a 'local-global' coherence can be imposed on the norms. This means that whenever a transition is coloured red for a given agent (because of some agent-specific permission law), the transition is deemed to be red overall. This constraint is imposed by adding the fact

    local_global.

to the action description. The action description of nC+ that contains all these additions is in the file emerson02.

pC+

pC+ extends C+ for the representation of authorization and obligation policies, and policy composition using the language PBel. (For PBel, see A simple and expressive semantic framework for policy composition in access control by Bruns, Dantas and Huth.) The language pC+, with implementation details and examples, is described in Policies, Norms and Actions by Craven. (The sample action descriptions referred to in that paper are here: pna01, pna02, pna03.)

Using pC+ necessitates a slight change in the specification of signatures for action descriptions. Action constants are now divided into three categories. (i) Regular action constants, declared as usual using ac/1, which represent actions not controlled by policies. (ii) 'Permission action constants', declared in a similar way using pac/1, which represent actions controlled by authorization policies. (iii) 'Obligation action constants', declared using oblpac/1, which represent actions subject both to event-condition-action rules and authorization policies. (We will call action constants that fall into categories (ii) and (iii) 'policy action constants'.)

Policy action constants should take the form 'S^X', where 'S' is the subject, who is performing some action 'X'. Typically 'X' itself has additional structure as 'A^T', where 'A' is the name of an action or operation that can be performed on a target 'T'. This extra structure is not necessary, however. The policy action constants in our example are specified as follows:

    ac(A^move).
    oblpac(A^writeTo^A1) :- A \= A1.
    domain(A^move, L).
    domain(A^move, ff).

Policy action constants should generally not be declared as 'exogenous': whether or not the action is performed depends on whether the authorization policy in place allows a request for the action to pass.

Aside from adjustments to the signature, pC+ requires the addition of several new kinds of information in source files. First, there should be definitions of the basic policies: these are named policies consisting of either all positive authorization rules, or negative authorization rules. For example, here is a basic negative authorization policy, called 'pol':

    pol @ {
        denied(emerson^writeTo^thoreau) if loc(emerson)=harvard
    }.

The law inside the curly brackets has a 'denied( )' constant in its head, and its body is a conjunction of atoms. If more than one law were included in a basic policy, this is written in the form:

    pol2 @ {
        ( denied(P1) if C1 :- B1 ),
            ...
        ( denied(Pn) if Cn :- Bn )
    }.

Positive authorization policies take the same form but with 'perm' in the head.

Secondly, there should be a declaration of what the top policy is (this is the policy used by the PDP to evaluate access requests). The top policy is typically defined as a composition of other policies; the other policies may be basic, or themselves defined in terms of more policies. Here is how the top policy is declared in our example domain:

    top ptop is (pol or (neg pol)).

The name of the top policy is 'ptop', and it is defined, in terms of the policy 'pol', as 'pol or (neg pol)'.

Definitions of other policies are made using expressions of the form

    policy P is Comp.

where 'P' is the name of a policy and 'Comp' is a policy composition expression, such as '(pol or (neg pol))', above. The names of negation, meet and join according to truth ordering are 'not', 'and', 'or'. The names of negation, meet and join according to the knowledge ordering are 'neg', 'meet' and 'join'. Binary operators are infix. (See Policies, Norms and Actions for more details on the language.)

Optional abbreviations of new policy composition operators can be made using the predicate pol_abbrev/2. For example, the operator '>', which we use often, is defined as:

    pol_abbrev(X > Y, X join ((neg (X join (not X))) meet Y) ).

Obligation policies (interpreted as event-condition-action rules) are written straightforwardly as C+ action dynamic laws with the constant 'obl( )' in the head. For example:

    caused obl(emerson^writeTo^thoreau) if turbulent(emerson).

Any action in an 'obl( )' constant must be declared as 'oblpac'.

An optional fact

    pdp_transparent.

in the source file means that constants representing the evaluation of all named policies will be included in the action description. Without this fact, only the overall decision for a request is represented.

The file emerson03 contains the causal laws, laws of nC+ (norms), and laws of pC+ (policies) mentioned so far.

Transition System Visualization

To visualize the transition system defined by the action description, use

    ?- trans2dot.

This will find all the states and transitions, write them as a .dot file, run graphviz on the .dot file, and show the results using evince.

The answers to individual queries can be visualized using q2dot/1 and q2dot/2. These take the same arguments as query/1 and query/2, but the solutions are written to a .dot file and then shown pictorially. The 'time' argument should always be 0 or 1 for visualized queries.

Options and Other Utilities

There are various options that can be set and other utilities for inspecting the action description currently loaded in iCCalc or mcLUCA.

Current values for options can be displayed by

    ?- options.

A value of an option can be set using

    ?- set_opt(OptionName, OptionValue).

Information about the current action description can be shown using the following predicates.