Jessica Calvo

Nicolas Carbonell

Olivier Scatton

Christophe Marzac

Nathalie Ganne-Carrie

Dominique Wendum

Hepatic nodular lymphoid lesion with increased IgG4-positive plasma cells associated with primary biliary cirrhosis: a report of two cases

Introduction

Nodular lymphoid lesion of the liver, also called nodular reactive lymphoid hyperplasia or pseudolymphoma is a rare condition that appears as liver nodules. Typically, it affects adult women and can be associated with an autoimmune disease, chronic hepatitis or a past history of malignancy. The pathogenesis of this lesion is so far unknown and is suggested to be autoimmune [START_REF] Sharifi | Nodular lymphoid lesion of the liver: an immune-mediated disorder mimicking low-grade malignant lymphoma[END_REF][START_REF] Takahashi | Reactive lymphoid hyperplasia of the liver in a patient with colon cancer: report of two cases[END_REF][START_REF] Zen | Hepatic pseudolymphoma: a clinicopathological study of five cases and review of the literature[END_REF]. Histologically, it consists of lymphoid tissue with lymphoid follicles, a dense lymphoplasmacytic infiltrate and clusters of epithelioid cells. The main differential diagnosis is low grade B-cell lymphoma, particularly marginal zone B-cell lymphoma [START_REF] Willenbrock | Nodular lymphoid lesion of the liver with simultaneous focal nodular hyperplasia and hemangioma: discrimination from primary hepatic MALT-type non-Hodgkin's lymphoma[END_REF]. Recently, some reactive lymphoid infiltrates with an increased number of IgG4 positive (+) plasma cells have been associated to IgG4-related disease [START_REF] Cheuk | IgG4-related Sclerosing disease: a potential new etiology of cutaneous pseudolymphoma[END_REF][START_REF] Guinee | Pulmonary nodular lymphoid hyperplasia (pulmonary pseudolymphoma): the significance of increased numbers of IgG4positive plasma cells[END_REF].

We herein report the first two cases of reactive lymphoid hyperplasia of the liver with an increased number of IgG4+ plasma cells in patients with primary biliary cirrhosis (PBC). We will discuss the relationship of these lesions with IgG4-related disease.

Clinical History

Case 1

A 70-year-old woman with a history of PBC presented with abdominal pain. She underwent an abdominal ultrasound which revealed a 23mm left lobe liver nodule. PBC was diagnosed six years before by the presence of cholestasis with type M2 antimitochondrial antibodies (> 1/640). Rheumatoid factor antibodies, Sjögren syndrome-A antibodies, Sjögren syndrome-B antibodies and antinuclear antibodies were negative. Hepatitis B and C serologies were negative. A liver biopsy performed at that time showed a Ludwig's stage 2 PBC. The patient was treated with ursodeoxycholic acid (15mg/kg/day) leading to the normalization of liver function tests (bilirubin, alkaline phosphatase, γ-glutamyltransferase, aspartate aminotransferase, alanine aminotransferase).

On the MRI, the lesion measured 23mm, was enhanced at the arterial phase with no wash out at the portal phase (figure 1a and1b). The liver was not dysmorphic and there was no sign of portal hypertension. On the PET-scan, the lesion appeared hypermetabolic without any other hypermetabolic foci. Alpha-fetoprotein and carcinoembryonic antigen serum levels were within normal ranges. Resection of the left lobe of the liver was performed.

Two years after the surgical resection, the patient had a lobular breast carcinoma treated by surgery, radiotherapy and letrozole. No other particular event occurred within the 3-year follow-up.

IgG4-related disease was not found in other organs and IgG4 serum levels measured after surgery were normal (<140 mg/dL).

Case 2

An 80-year-old woman with a history of PBC diagnosed 2 years before underwent a routine liver ultrasound, which revealed a 13mm hypoechoic right liver nodule. PBC was diagnosed by the presence of cholestasis with type M2 antimitochondrial antibodies (1/640). A liver biopsy was performed and showed a Ludwig's stage 2 PBC. The patient was treated with ursodeoxycholic acid (15mg/kg/day), leading to liver function tests normalization.

The patient was also diagnosed with Sjögren syndrome with xerostomia and positive Sjögren syndrome antibodies. The CT scan and MRI showed an arterial phase enhancement of the liver lesion with a portal phase wash out, suggesting hepatocellular carcinoma (figure 2a and2b). A biopsy of the lesion followed by radiofrequency ablation was performed. A concomitant biopsy in the non-tumoral liver was also performed.

Three years after radiofrequency ablation, there was no recurrence.

IgG4-related disease was not found in other organs and IgG4 serum levels, measured after radiofrequency ablation, were normal (<140 mg/dL).

Materials and Methods

Formalin fixed pararffin embedded (FFPE) tissues were cut into 3μm-thick sections and were submitted for H&E, Ziehl-Neelsen, Gomori-Grocott, orcein stainings, immunohistochemistry (IHC) and in-situ hybridization.

IHC was performed using a Bond-Max automated immunostainer (Leica Microsystems) using the following antibodies with prior antigen retrieval (10mM citrate buffer pH 6): CD3 (Neomarker, 1:300), CD5 (Novocastra, 1/50), CD20 (Novocastra, 1:350), CD21 (Novocastra, 1:100), CD23 (Novocastra, 1:50), CD43 (Dako, 1:75), CD138 (Dako, 1:100), IgG4 (Binding Site, 1:200), IgG ( Dako, 1:1000) , kappa (DB-Biotech, 1:500), and lambda (DB-Biotech, 1:2000) light chains. Epstein Barr virus (EBV) detection was performed by in-situ hydridization using an EBV-encoded RNA probe (EBER) (Leica, ISH EBER ready to use oligonucleotide probe). IgG4+ plasma cells were counted on the three HPFs (x400, 0.24mm 2 per field) with the highest number of IgG4+ plasma cells, and the average was determined. IgG plasma cells were counted in the same way on the same three fields to provide the IgG4/IgG ratio [START_REF] Deshpande | Consensus statement on the pathology of IgG4-related disease[END_REF].

DNA was extracted from the FFPE tissue (QIAsymphony DSP DNA Mini Kit, Qiagen). Clonal immunoglobulin heavy chain rearrangement was searched by using three VH-JH fluorescent multiplex PCR followed by fragment length analysis, according to BIOMED-2 standardization protocol [START_REF] Van Dongen | Design and standardization of PCR primers and protocols for detection of clonal immunoglobulin and T-cell receptor gene recombinations in suspect lymphoproliferations: report of the BIOMED-2 Concerted Action BMH4-CT98-3936[END_REF].

Results

Case 1

Grossly, the lesion measured 18mm, appeared white, homogeneous and well circumscribed (figure 1c).

Histologically, it consisted of lymphoid follicles with a dense lymphoplasmacytic infiltrate containing abundant regular plasma cells and clusters of epithelioid histiocytes, forming grannulomas (figure 1d). Fibrous tissue was scarce within the lesion, with no storiform pattern. Obliterative phlebitis was not identified.

No infectious pathogen was identified on Ziehl-Neelsen and Gomori-Grocott stainings. IHC profile showed a majority of CD138+ cells, with CD20+ and CD3+ small lymphocytes. There was no abnormal expression of CD5 or CD23. The Kappa/Lambda ratio of plasma cells was normal with a polyclonal pattern. EBV encoded small RNAs were not detected. The IgG4+ plasma cell count was 82 per HPF (figure 1e) and the IgG4/IgG ratio was > 40%. There was no rearrangement of immunoglobulin heavy chains using FR1/JH, FR2/JH, and FR3/JH primers in the lymphoid tissue. In the non-tumoral liver, there were a few fibrous septa, mild steatosis, lymphoplasmacytic portal inflammation with lymphocytic destructive cholangitis (figure 1f) and mild interface hepatitis suggestive of stage 3 PBC. There were no IgG4+ plasma cells in the non-tumoral liver (figure 1g) Case 2

The histological examination of the biopsy specimen showed the same pattern as in case 1, with abundant nonatypical plasma cells and small lymphocytes. There were some epithelioid cells and a slight non storiform fibrosis (figure 2c). The Kappa/Lambda ratio of plasma cells was normal with a polyclonal pattern. The IgG4+ plasma cells count was 76 per high power field and the IgG4/ IgG ratio was > 40%. The non-tumoral liver biopsy showed a Ludwig's stage 2 PBC with a dense portal lymphoplasmacytic infiltrate, lymphocytic and granulomatous cholangitis (figure 2e), moderate interface hepatitis and periportal fibrosis without bridging. There were no IgG4+ plasma cells in the non-tumoral liver (figure 2f).

Discussion

These two cases of nodular lymphoid lesions of the liver. showed a typical histological aspect with a dense lymphoplasmacytic infiltrate, lymphoid follicles, and epithelioid granulomas with no rearrangement of immunoglobulin heavy chains using FR1/JH, FR2/JH [START_REF] Sharifi | Nodular lymphoid lesion of the liver: an immune-mediated disorder mimicking low-grade malignant lymphoma[END_REF][START_REF] Takahashi | Reactive lymphoid hyperplasia of the liver in a patient with colon cancer: report of two cases[END_REF][START_REF] Zen | Hepatic pseudolymphoma: a clinicopathological study of five cases and review of the literature[END_REF]. However, there were abundant IgG4+ plasma cells within these lesions, which, to our knowledge, has not been previously described in nodular lymphoid lesions of the liver.

Our observations led us to consider whether these lesions may be manifestation of IgG4-related disease or not.

Importantly, an increasing number of lesions rich in IgG4 + plasma cells have been identified since the concept of IgG4-related disease has emerged. However, these lesions do not always belong to the spectrum of IgG4-associated systemic disease. For instance, abundant IgG4+ plasma cell infiltrate has been identified in primary sclerosing cholangitis, inflammatory bowel disease, rheumatoid arthritis and carcinomas [START_REF] Zhang | IgG4+ plasma cell infiltrates in liver explants with primary sclerosing cholangitis[END_REF][START_REF] Strehl | Numerous IgG4-positive plasma cells are ubiquitous in diverse localised non-specific chronic inflammatory conditions and need to be distinguished from IgG4related systemic disorders[END_REF][START_REF] Virk | Tissue IgG4-positive plasma cells in inflammatory bowel disease: a study of 88 treatment-naive biopsies of inflammatory bowel disease[END_REF][START_REF] Kimura | Pathologic significance of immunoglobulin G4-positive plasma cells in extrahepatic cholangiocarcinoma[END_REF].

The diagnosis of IgG4-related disease is based on a set of both clinical and histopathological features. The typical histological features combine a dense lymphoplasmacytic infiltrate with abundant IgG4+ plasma cells, storiform fibrosis and obliterative phlebitis [START_REF] Deshpande | Consensus statement on the pathology of IgG4-related disease[END_REF][START_REF] Stone | IgG4-related disease[END_REF]. Nevertheless, some lesions are suggested to belong to the spectrum of IgG4-related disease even though they have atypical histological aspects [START_REF] Wong | IgG4-related sclerosing disease of the small bowel presenting as necrotizing mesenteric arteritis and a solitary jejunal ulcer[END_REF][START_REF] Bateman | Immunoglobin G4hepatopathy: association of immunoglobin G4-bearing plasma cells in liver with autoimmune pancreatitis[END_REF].

In our two cases, despite a dense lymphoplasmacytic infiltrate with an increased number of IgG4+ plasma cells (> 50/HPF on gross specimen, and > 10/ HPF on biopsy with a IgG4/IgG ratio > 40%), some characteristic features of IgG4-related disease were missingi.e. lack of significant fibrosis and obliterative phlebitis.

According to Deshpande et al. diagnostic criteria for IgG4-related disease, our cases belong to the « probable histological feature of IgG4-related disease » category [START_REF] Deshpande | Consensus statement on the pathology of IgG4-related disease[END_REF]. To be more consistent, the diagnosis of IgG4-related disease requires additional clinical, radiological and/or serological evidence. They were all missing in our cases: the serum levels of IgG4 were normal at the time of local ablation of the focal lesion and the patients had no other organ manifestation of IgG4-related disease, in particular no pancreatic, biliary, salivary, cutaneous or pulmonary lesion, either at baseline or 3 years after local treatment.. The response to corticosteroid therapy can also be a strong argument to underpin the diagnosis of IgG4-related disease, but it could not be assessed in our cases since the lesions were ablated.

The histological features in our cases also included the presence of prominent granulomas. Granulomas are usually regarded as a feature that is not seen in IgG4-related disease. In most settings their presence would make this diagnosis very unlikely, even though Bateman et al. recently highlighted the fact that granulomas may be seen in lymph nodes in IgG4-related disease [START_REF] Bateman | Immunoglobin G4hepatopathy: association of immunoglobin G4-bearing plasma cells in liver with autoimmune pancreatitis[END_REF].

The pathological aspects of the non-tumoral liver in our cases did not provide any evidence for liver IgG4 hepatopathy. According to Umemura et al., histological findings in the liver of patients with IgG4-related pancreatitis can have several patterns: 1) a portal inflammation pattern, with intense portal inflammation with or without interface hepatitis; 2) a large duct damage pattern, characterized by bile ductular proliferation, neutrophilic infiltration and edematous change in the portal areas; 3) a portal sclerosis pattern, exhibiting dense portal sclerosis with scarce portal inflammation; 4) a lobular hepatitis pattern, showing lobular inflammation with hepatocellular necrosis resembling viral hepatitis; or 5) a cholestatic pattern, with canalicular cholestasis predominantly in the centrilobular area [16]. A perivenular accentuation of the portal infiltrate and portal based fibroinflammatory nodules have also been described in the liver of patients with IgG4-related cholangitis [START_REF] Deshpande | IgG4-associated cholangitis: a comparative histological and immunophenotypic study with primary sclerosing cholangitis on liver biopsy material[END_REF].

The only common feature in all these patterns is a prominent IgG4+ plasma cell infiltrate.

In our cases, the pathological aspects of the non-tumoral liver could be consistent with the portal inflammation pattern, but its lack of IgG4+ plasma cells, combined with granulomatous cholangitis and typical serum immunological abnormalities (Anti-mitochondrie M2 antibodies > 1/640 ) , precludes the diagnosis of liver IgG4-related disease and was typical of PBC [16,[START_REF] Deshpande | IgG4-associated cholangitis: a comparative histological and immunophenotypic study with primary sclerosing cholangitis on liver biopsy material[END_REF].

All these arguments suggest that our lesions may not be a manifestation of IgG4-related disease. However, conversely, it has been suggested that pulmonary pseudolymphoma might be a form of IgG4-related sclerosing disease with no other typical feature than a rich IgG4+ plasma cell infiltrate and a high IgG4/IgG ratio [START_REF] Guinee | Pulmonary nodular lymphoid hyperplasia (pulmonary pseudolymphoma): the significance of increased numbers of IgG4positive plasma cells[END_REF]. The histological findings of this lung lesion have many similarities with our cases, namely lymphoid follicles with a variable degree of fibrosis, sheets of interfollicular plasma cells and the absence of obliterative phlebitis.

A specific finding in our two lesions was their occurrence in patients with PBC. Whereas reactive nodular lymphoid hyperplasia has been described to be associated with PBC, IgG4+ plasma cell infiltrates have not been identified in PBC livers [START_REF] Chung | Identification and characterization of IgG4-associated autoimmune hepatitis[END_REF]. The Th1 and Th17 signaling pathways have been associated with the pathogenesis of PBC [START_REF] Yang | IL-12/Th1 and IL-23/Th17 biliary microenvironment in primary biliary cirrhosis: implications for therapy[END_REF]. By contrast, the immunological profile of IgG4-related disease is a Th2-cell-dominant immune response in affected sites and in peripheral blood T-cell lymphocytes [START_REF] Miyake | Peripheral CD4+ T cells showing a Th2 phenotype in a patient with Mikulicz's disease associated with lymphadenopathy and pleural effusion Modern rheumatology / the Japan[END_REF][START_REF] Zen | Th2 and regulatory immune reactions are increased in immunoglobin G4-related sclerosing pancreatitis and cholangitis[END_REF]. However, the pathogenesis of an IgG4+plasma cell rich lesion in an organ affected by a Th1-related auto-immune disease, namely PBC, is unclear.

To conclude, we described the first two cases of nodular lymphoid lesions of the liver with abundant IgG4+ plasma cells occurring in patients with PBC. It seems unlikely that these lesions are manifestation of IgG4related disease. However, because the pathogenesis of both nodular lymphoid lesions and IgG4-related disease remain unclear, studying IgG4+ plasma cell infiltrates in a larger number of nodular lymphoid lesions and determining the precise pathogenesis of IgG4-related disease are necessary.

Acknowledgments

The authors thank Dr Jacqueline Fontugne for her assistance in revising the manuscript.


Lenz Belzner
email: belzner@pst.ifi.lmu.de

Verifiable Decisions in Autonomous Concurrent Systems

Being able to take decisions at runtime is a crucial ability for any system that is designed to act autonomously in uncertain or even unknown environments. This autonomy necessitates to formally check system properties at design time to ensure avoidance of problems or even harm caused by the system at runtime. This paper is about the formal specification of concurrent systems that are capable of reasoning about the consequences of their actions, enabling them to coordinate and decide on what to do autonomously. A non-deterministic procedural action programming language is defined to constrain system behaviour at design time. Rewriting logic is employed to construct and evaluate possible traces of programs in a decision-theoretic manner, allowing agents to perform goal-based actions autonomously at runtime as well as providing possibilities to model-check system properties at design time.

Introduction

Concurrent multiagent systems designed to act autonomously in highly dynamic, non-deterministic environments expose a number of requirements that have to be addressed by modelling and specification approaches. In fact, their design has to enable a system to reason about possibly uncertain outcomes of its actions in order to decide what behaviour to perform at runtime. This kind of cognitive ability requires specification of knowledge about actions' preconditions and effects. Algorithms have to be provided to enable a system to evaluate and decide on particular behavioural alternatives. Also, in the presence of multiple agents that share the same environment, the issues of concurrency and synchronization have to be accounted for by any specification approach.

Along with the specification of knowledge about actions and uncertainty, it should be possible to constrain the behaviour of an autonomous system at design time. To this end, non-deterministic action programming languages [START_REF] Thielscher | Action Programming Languages[END_REF] allow for specification of behavioural constraints. In fact, non-deterministic programs allow to specify plan sketches that can be seen as behavioural alternatives provided to a system. These alternatives can then be evaluated in the context of a situation that a system finds itself in at runtime.

For systems that act autonomously, formal verification of properties at design time, e.g. by model checking, is a valuable source of information for design choices and error detection. In this paper, the formalization of knowledge and behavioural constraints for ensembles is realized in rewriting logic [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF][START_REF] Clavel | All About Maude -a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic[END_REF][START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF]. Domain knowledge is represented as a relational Markov Decision Process [START_REF] Puterman | Markov Decision Processes: Discrete Stochastic Dynamic Programming[END_REF][START_REF] Boutilier | Symbolic dynamic programming for first-order mdps[END_REF]; a non-deterministic action programming language is defined to allow for specification of behavioural constraints. The rewriting logic concepts of matching and rewriting are employed to provide to a system the ability to reason about the consequences of its behaviour. A number of problems that are typical for cognitive systems are addressed in this paper:

-Specification of knowledge about actions. Besides providing to a system information about pre-and postconditions of actions, it is necessary that the system knows what properties of the environment remain unchanged. In static logics like first-order logic, this is a non-trivial issue known as the frame problem [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intelligence[END_REF]. -Legality & projection. If a system is provided with the ability to choose from various behavioural alternatives, this may lead to action choices that cannot be executed at runtime due to precondition violations. To decide whether a certain behavioural trace is legal (i.e. executable w.r.t. action preconditions), a cognitive agent has to be capable of deciding whether certain properties of the environment hold as consequences of its actions; an ability that is known as projection [START_REF] Reiter | Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems[END_REF]. -Trace evaluation & system property verification. Non-deterministic action programs are employed to constrain system behaviour, giving raise to various execution traces, thus enabling a system to evaluate behavioural alternatives w.r.t. its goals. Also, the consequences arising from the execution of traces can be used to verify properties of the given action program at design time. -Concurrency. When multiple agents interact dynamically at runtime, the issues of concurrency, synchronization and coordination arise, especially in the presence of sharing. Reasoning about concurrent execution should be possible with specified knowledge about a domain; also, the legality and projection problems have to be dealt with in the presence of concurrency.

This paper extends previous work on action programming in rewriting logic [START_REF] Belzner | Action programming in rewriting logic[END_REF] by decision-theoretic concepts, and discusses in more detail the integration of concurrency and coordination. Also, an approach towards probabilistic modelchecking for action programs is discussed. The paper is outlined as follows. Section 2 introduces rewriting logic and action programming. Section 3 discusses the specification of knowledge and behaviour for autonomous concurrent systems in terms of a rewrite theory, and defines how the concepts of matching and rewriting are employed to interpret and reason about the specification. Section 4 discusses how to perform model checking of action programs for typical desirable system properties. A short example illustrating the approach is given in section 5. In section 6, related work is compared with the presented specification approach. Finally, section 7 summarizes the results and gives a brief outlook on further research venues. This section gives a brief introduction to rewriting logic (section 2.1) and action programming (section 2.2).

Rewriting Logic

The core concept of rewriting logic are rewrite theories (Σ, A∪E, R, φ) [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF][START_REF] Clavel | All About Maude -a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic[END_REF][START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF]. Σ is a signature defining sorts, sort-orders and operations to build terms from sorts in the signature. A are axiomatic definitions for operations in Σ like associativity, commutativity, idempotency or identity, and E specifies a set of equations for terms in Σ. A ∪ E defines equivalence classes for terms, representing the static structure of the rewrite theory. R is a set of possibly conditional rewrite rules that specify the theory's dynamics. Finally, φ is a function from operations to natural numbers that defines which arguments of an operation are frozen, meaning that no rewriting will take place on this argument.

Term rewriting with rewrite theories is performed by matching terms with rules. In rewriting logic, matching is performed modulo axioms with extensions (called Ax-matching). For example, consider an operation • that is associative and commutative. Then, the term a

•b•c would Ax-match the term c•a, because a • b • c = A c • a • b
due to axioms for •, and obviously c • a is a subterm of the given term. If terms contain variables, matching applies if there is a substitution that renders a subterm of a given subject term equal to a term to be matched; thus, a more concrete term matches a more general one.

Rewrite rules are of the form l → r if Conditions, where l and r are terms in Σ that have an equal least sort, and Conditions can either be boolean expressions, matching conditions (true if a term t Ax-matches a term t , denoted t := t ) and rewriting conditions (true if a term t rewrites to a term t according to rules in R, denoted t → t ). Rewriting of a subject term t is performed if a non-variable subterm of t matches a rule's left-hand side, and the conditions of the rule hold for the particular matching substitution. The matched subterm is then replaced by the rules right-hand side. Rewriting of a term to its normal form, where no more rewrite rules can be applied, is denoted by t → ! t .

As Ax-matching a term with rules may result in different matched subterms and substitutions, rewriting can naturally express non-determinism. Also, as multiple rules may be applied to different subterms in parallel, rewriting logic is considered an intuitive way to deal with concurrency [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF].

As long as some admissibility requirements are satisfied (e.g. if there are no fresh variables in a rule's right-hand side), the process of rewriting can be performed computationally. This fact has led to the development of the termrewriting language Maude [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF][START_REF] Clavel | All About Maude -a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic[END_REF]. Rewrite theories can straightforwardly be implemented as Maude modules. The language provides a built-in breadth-first search command to compute all possible rewrites of a term, where search depth and the number of desired solutions are parametrized. This approach can for example be used to perform automated state-space search on rewrite theories in order to model-check a given specification (see section 4).

Action Programming

Action programming is "the art and science of devising high-level control strategies for autonomous systems which employ a mental model of their environment and which reason about their actions as a means to achieve their goals" [START_REF] Thielscher | Action Programming Languages[END_REF].

Action programming allows to specify non-deterministic programs that can be considered as a plan sketch, roughly outlining desired behaviour of a system without committing to a certain trace of actions. In other words, an action program defines a constrained space of behavioural alternatives. To allow a system to reason about these alternatives at runtime, a domain specification is provided that contains definitions of fluents (i.e. state properties) that are subject to change (e.g. due to action execution) as well as actions in terms of their preconditions and effects, which may also be non-deterministic. This knowledge can then be employed by the system to decide what to do at runtime.

For example, consider fluents x, y and z, and actions α and β. Informally, assume x, y → α z, x → β y and y → β z, denoting an action's precondition and (non-deterministic) effects. Then, given the action program α # β where # is a non-deterministic choice operator and a current situation where x and y hold, an agent can derive that executing α will lead to a situation where z holds, and that execution of β could result in a state where either y holds (as x, y → β y, y) or where x and z hold (according to the latter specification of β).

Influential action programming formalisms are the situation calculus with its language Golog [START_REF] Reiter | Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems[END_REF] and the fluent calculus and its language Flux [START_REF] Thielscher | Flux: A logic programming method for reasoning agents[END_REF]. The situation calculus employs a fluent-wise regressive specification of action effects known as successor state axioms, where the frame problem is explicitly handled by also stating under what conditions some fluent does not change. States are not explicitly managed, but rather the notion of a situation is used to test whether a fluent holds after execution of an action program. On the other hand, the fluent calculus uses a progressive, action-wise specification of domain dynamics by defining modifications of an associative-commutative representation of a state that arise due to action execution.

Decisions in Autonomous Concurrent Systems

As mentioned in section 2.2, to provide to a system the ability to reason in terms of action programming, specification of domain dynamics as well as a language to define behavioural alternatives are necessary. In section 3.1, the encoding of domain knowledge in terms of a rewrite theory encoding a relational MDP is discussed. Section 3.2 defines a non-deterministic, procedural action programming language that employs the specified rewrite theory to construct trace consequences through Ax-matching and rewriting (see section 2.1), and introduces the notion of a trace's value, thus enabling systems to reason about action preferences. Section 3.3 deals with the explicit treatment of projection, and provides definitions for branching and loops. Section 3.4 discusses action programming with concurrency in the presence of sharing, allowing for agent synchronization and coordination.

RMDPs as Rewrite Theories

For specification of non-deterministic domain dynamics, the proposed approach employs the notion of a relational MDP. A relational MDP is a tuple (S, A, T, R), where S is a set of relational states, A a set of actions, T : S × A × S → [0; 1] is a transition function specifying the probability that execution of a particular action in a state results in another one, and R : S → R is a reward function. To encode such a relational MDP as a rewrite theory, a set of fluents F is defined (see section 2.2), from which the set of states Σ is built by means of the following syntax. Both ∧ and ∨ are associative and commutative with identity element σ . The equivalence classes of terms in Σ can be considered the set of states S of a relational MDP.

Σ := σ f ∈ F ¬Σ Σ ∧ Σ Σ ∨ Σ
States annotated with probability are denoted by σ p := (σ ∧ prob(p)) ∈ Σ, with a fluent prob : [0; 1] → F encoding the probability of a system being in state σ. The set of states annotated with a probability fluent is denoted by Σ P .

The transition function T is encoded in terms of rewrite rules. If there are n non-deterministic transitions in T that define the effects of executing action α in state σ each leading to a state σ i with probability p i , i ∈ {1, ..., n}, a rule is defined for each of them in the form Σ P ×A → Σ P as follows (with

n i=1 p i = 1). σ p i × α → σ i p * T (σ,α,σ i ) . (1)
The states σ and the σ i can be considered as pre-and postconditions of action α.

Note that this notation of transitions provides a solution to the frame problem [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intelligence[END_REF], as subject terms are matched with extension when applying rules. Thus, there is no necessity to explicitly specify state properties that remain unchanged by application of a rule.

Example 1. (Action rules) A rule for defining an action move that moves a robot R at position P (denoted by a fluent pos : Robot × Position → F ) to a desired position P with a probability of 0.9 and has no effect otherwise is specified by the following rules.

pos(R, P ) p × move(R, P ) → pos(R, P ) p * 0.9 .

pos(R, P ) p × move(R, P ) → pos(R, P ) p * 0.1 .
Finally, a MDP's reward function R can simply be encoded in terms of an operation together with corresponding equations. For example, considering a variable S of sort state1 , the equations R(pos(r, p)∧S) = 1, R(S) = 0 [otherwise] specify a reward of 1 for states where robot r is at position p and zero reward for all other states.

Progressive Action Programming

This section describes how to constrain system behaviour in terms of an action program, and how a system can construct and evaluate behavioural alternatives according to these constraints when given a rewrite theory as domain specification as outlined in section 3.1. To this end, a procedural non-deterministic action programming language is defined with syntax Π.

Π := π α ∈ A Π;Π Π#Π
Here, π denotes the empty program, α is an action from the domain specification, ; is an associative sequential operator, and # is an associative-commutative non-deterministic choice operator, offering behavioural alternatives to a system executing the program. Both operators have π as identity element.

To allow for numerical evaluation of states, these are annotated with a value (i.e. gathered reward), denoted by σ p×v := (σ p ∧ value(v)) ∈ Σ with a fluent value : R → F encoding the value v gathered in a state σ. The corresponding set of states annotated with probability and value is denoted by Σ P ×V .

Program interpretation and trace evaluation is then performed by rewriting configurations Σ P ×V × Π × Π × N that consist of a current state, an action program to be evaluated, an action trace leading to the current state and a planning horizon. The set of configurations is denoted as Ξ. For ease of notation, functions σ ξ , p ξ , v ξ , π ξ , τ ξ , h ξ are defined, taking as parameter a configuration ξ := σ p×v × π × τ × h, returning its respective values, e.g. σ ξ (ξ) = σ.

To compute possible consequences of executing for h steps an action program π in a particular state σ, an initial configuration ξ init := σ 1.0×0.0 × π × π × h is rewritten according to the following rules, resulting in a set of configurations

{ξ ξ init → ! ξ ∈ Ξ}. 2 σ p×v ∨ i σ i pi×vi → σ p×v .
(2)

σ p×v × α × τ × h → σ p ×v × π × (τ ;α) × (h -1) if h > 0 ∧ σ p × α → σ p ∧ v := v + R(σ ) . (3)
σ p×v × (π 1 ;π 2 ) × τ × h → σ p ×v × π 2 × τ × h if σ p×v × π 1 × τ × h → σ p ×v × π × τ × h . ( 4
)
σ p×v × (π 1 #π 2 ) × τ × h → σ p×v × π 1 × τ × h . (5)
As state disjunction is associative and commutative, rule (2) rewrites a state in disjunctive normal form to all its conjunctive subterms, leading to subsequent rewriting of configurations only containing conjunctive states. Note that disjunctive normal form for states can easily be assured by specifying according equations for state-terms. Rule (3) rewrites a configuration containing a single action α as program if the planning horizon has not yet been reached and the action's preconditions are satisfied by the current state. Satisfaction of preconditions is tested by rewriting the current state σ p with the given action according to the transition rules for actions in the domain. If σ p × α can be rewritten, the preconditions are satisfied, and any rewards of the reached state are added to v 3 . Otherwise rewriting terminates, thus solving the legality problem by Ax-matching left-hand sides of rewrite rules encoding the transition function of a relational MDP with σ p × α. 4 Note that Ax-matching is highly efficient; for ac-terms typically met in practice, its complexity does not exceed O(log n), where n is term size [START_REF] Eker | Associative-commutative rewriting on large terms[END_REF]. Ax-matching also results in a non-deterministic argument pick if a parameter of the action that is to be processed is a variable.

Rewriting of sequential programs determines all configurations that can result by executing the sequence's head, which are then further rewritten according to the sequence's tail (rule (4)). Choice programs are rewritten according to rule [START_REF] Puterman | Markov Decision Processes: Discrete Stochastic Dynamic Programming[END_REF], that will rewrite a configuration according to all possible program choices as the choice operator is associative and commutative.

In contrast to configurations for which rewriting terminated due to precondition violation, rewriting also terminates for a configuration ξ exposing h ξ (ξ) = 0 (due to rule (3)) or π ξ (ξ) = π (because there is no rule for interpreting π ). Thus, these properties can be used to define the set of legally terminating configurations Ξ ↓ arising from rewriting an initial configuration ξ init ∈ Ξ according to program traces where no action precondition is violated.

Ξ ↓ (ξ init ) := {ξ ξ init → ! ξ ∧ (π ξ (ξ) = π ∨ h ξ (ξ) = 0)}
The set of legally terminating program traces T ↓ for an initial configuration ξ init ∈ Ξ is defined as follows.

T ↓ (ξ init ) := {τ ξ ∈ Ξ ↓ (ξ init ) ∧ τ ξ (ξ) = τ )}
Similarly, the set of configurations yielding a particular, legally terminating trace Ξ τ ↓ is defined.

Ξ τ ↓ (ξ init ) := {ξ ξ ∈ Ξ ↓ (ξ init ) ∧ τ ξ (ξ) = τ }
The expected value of a legally terminating trace V e is the sum of expected values (which is the product of probability and value) of its non-deterministic outcomes.

V e (τ, ξ init ) := ξ∈Ξτ ↓ (ξinit) (p ξ (ξ) * v ξ (ξ)) ( 6
)
3 When rewards are specified action-wise, i.e. R : Σ × A × Σ, the computation of v in the condition of rule (3) changes to v := R(σ, α, σ ). 4 To allow for Ax-matching of states and actions technically, conjunction of fluents and concurrency of actions (see section 3.4) are implemented in terms of a single associative-commutative operation, e.g. • : state → state, with sorts fluent and action being subsorts of sort state. I.e.

σ ∧σ = σ •σ , σ ×α = σ •α, α α = α•α .
The legal termination probability P ↓ of a particular trace is the sum of all probabilities of configurations that yield the trace.

P ↓ (τ, ξ init ) := ξ∈Ξτ ↓ (ξinit) p ξ (ξ) (7)
Summarizing, given a domain specification and an initial configuration (i.e. a current state 5 , an action program and a planning horizon), rules (2) to [START_REF] Puterman | Markov Decision Processes: Discrete Stochastic Dynamic Programming[END_REF] together with the definitions for V e and P ↓ enable a system to perform the following tasks: (i) Computation of all program traces and their consequences. (ii) Determination of expected values for traces. (iii) Determination of legal termination probability of a particular trace.

Example 2. (Expected trace values and legal termination probability) Consider the rule for action move from example 1. Let S be a variable of sort Σ and r(pos(R, sa) ∧ S) = 1.0 (0 otherwise). Consider ξ init = pos(r, pos) 1.0×0.0 × move(r, sa) × π × 1. Then, expected value and legal termination probability of a possible trace of the program move(r, sa) that tries to move a robot r to the safety area sa compute as follows when executing it in a state where r is at position pos (with pos = sa). ξ init → pos(r, sa) 0.9×1.0 × π × move(r, sa) × 0 . ξ init → pos(r, pos) 0.1×0.0 × π × move(r, sa) × 0 .

V e (move(r, sa), ξ init ) = 0.9 * 1.0 + 0.1 * 0.0 = 0.9 . P ↓ (move(r, sa), ξ init ) = 0.9 + 0.1 = 1.0 .

Projection, Branching and Loops

The projection problem is to decide whether a certain property holds in a state or not (e.g. after a number of actions have been executed). As discussed in section 3.2, when interpreting action execution a state term is updated to yield the information about the resulting state. Thus, the projection problem reduces to deciding whether a property holds in a given state term. This is easily solved in rewriting logic: It suffices to check whether a given condition term in Σ Axmatches a particular state term for a substitution of variables θ. To this end, state subsumption (denoted by ) is defined as follows.

σ ? σ → θ if σ ? /θ := σ . σ ? σ ⇔ ∃θ : σ ? σ → θ . σ ? σ ⇔ ∃θ : σ ? σ → θ .
A state σ ? ∈ Σ thus subsumes another state σ ∈ Σ if its corresponding state term is more general than the state term of σ, which is checked by Axmatching the two terms. With this definition of state subsumption, operations are introduced for action programs that check whether a condition holds (or does not hold, respectively) at a particular stage of execution. The syntax for action programs is extended as follows.

Π ? := Π ?(Σ){Π ? } ¬?(Σ){Π ? } if Σ then Π ? else Π ? end if while Σ do Π ? end while
Interpretation of ?(σ ? ){π} succeeds if there is a substitution θ for which a condition σ ? subsumes the state of the current configuration to be rewritten. If so, the variable substitutions for which the condition hold are applied to the argument action program π (rule ( 8)). Similarly, rewriting ¬?(σ ? ){π} succeeds if there is no such substitution (rule ( 9)).

σ p×v ×?(σ ? ){π} × τ × h → σ p×v × π/θ × τ × h if σ ? σ → θ . ( 8
)
σ p×v × ¬?(σ ? ){π} × τ × h → σ p×v × π × τ × h if σ ? σ . (9)
With these operations, conditional branching can be defined as a macro.

if σ ? then π 1 else π 2 end if = ?(σ ? ){π 1 }#¬?(σ ? ){π 2 } . (10)
Testing whether a condition σ ? holds in (i.e. subsumes) a particular state σ also allows for interpretation of loops. If σ ? subsumes σ for a substitution θ, the loop body will be executed with θ applied, followed by the loop itself; otherwise, the loop reduces to the empty program.

σ p×v × while σ ? do π end while × τ × h → σ p×v × π/θ;while σ ? do π end while × τ × h if σ ? σ → θ .

(11)

σ p×v × while σ ? do π end while × τ × h → σ p×v × π × τ × h if σ ? σ . (12)

Concurrency

To allow for specification of action programs for agents that act concurrently, the set of actions is extended to A := α A A A where is associativecommutative with identity α and denotes parallel execution of actions. Programs are allowed to be executed in parallel as well: Π := Π ? (A/A ) Π Π , where the syntax of programs in Π ? is extended to allow for parallel actions.

As action rules are applied sequentially to the current state term when rewriting, it is necessary to lock changing subterms of the state term to model true concurrency, disallowing interleaving application of actions that would result in race conditions. To this end, action dynamics as in rule (1) (see section 3.1) are automatically compiled to rules of form ( 13), explicitly denoting which fluents of the precondition σ are changed by action execution and which ones are left unchanged. Changed fluents are locked by an operation φ : Σ → Σ, φ(σ) ∧ φ(σ ) = φ(σ ∧ σ ), keeping them from being further matched with parallel actions' preconditions. For instance, grab(r1, o) drop(r2, o) should always be considered illegal, as at least one precondition is violated in any case before applying any of the actions; if interleaving rewriting was performed without locking state changes, the application of drop would in turn render grab executable (and vice versa), which is something that should not occur when the actions are considered truly concurrent. I.e., locking of changed properties resembles a precondition check before any action is applied and a check of postconditions after application of all actions. Note that, if interleaving concurrency is to be modelled, locking of changing state properties can simply be dropped. Interleaving is then achieved by the non-deterministic application of rewrite rules for action dynamics from the domain specification.

σ p × α → σ i p * T (σ,α ,σ i ) where σ i = φ(σ i changed ) ∧ σ i unchanged . (13
Concurrent action programs are normalized to sequential and choice terms as shown in equations ( 14) and ( 15) (for α i ∈ A , π i ∈ Π ). Due to this normalization, interpretation of sequences and choices (rules (4) and [START_REF] Puterman | Markov Decision Processes: Discrete Stochastic Dynamic Programming[END_REF], see section 3.2) can be performed without rule modification by rewriting configurations with concurrent action programs.

(π 1 #π 2 ) π 3 = (π 1 π 3 )#(π 2 π 3 ) . ( 14
) (α 1 ;π 1 ) (α 2 ;π 2 ) = (α 1 α 2 );(π 1 π 2 ) . (15)
Rewriting (i.e. interpretation) of a parallel action (rule (3) for domains without concurrency, see section 3.2) resulting from transformation of a concurrent action program according to equation ( 15) is changed to account for resolution of locked state properties arising from rewriting according to rules of form ( 13) that specify action dynamics for concurrent domains.6

σ p×v × α × τ × h → (σ 1 ∧ σ 2 ) p ×v × π × (τ ;α ) × (h -1) if h > 0 ∧ σ p × α → (φ(σ 1 ) ∧ σ 2 ) p ∧ v := v + R(σ 1 ∧ σ 2 ) . (16)
Example 4. (Concurrency) Consider the move action from example 1. The example shows rewriting a state according to a concurrent action that tries to move two robots to a position p 3 , illustrating the evaluation of the rewrite condition in rule [START_REF] Hölldobler | A logic-based approach to dynamic programming[END_REF]. Rewrite results in the following set of states matching the conditions right-hand side (i.e. all actions have been rewritten). Note that depending on the outcome of actions, different state properties are locked.

(pos(r 1 , p 1 ) ∧ pos(r 2 , p 2 )) p × move(r 1 , p 3 ) move(r 2 , p 3 ) → φ(pos(r 1 , p 3 ) ∧ pos(r 2 , p 3 )) p * 0.9 * 0.9 ∨ (φ(pos(r 1 , p 3 )) ∧ pos(r 2 , p 2 )) p * 0.9 * 0.1 ∨ (pos(r 1 , p 1 ) ∧ φ(pos(r 2 , p 3 ))) p * 0.1 * 0.9 ∨ (pos(r 1 , p 1 ) ∧ pos(r 2 , p 2 )) p * 0.1 * 0.1 .

If particular actions require synchronization of agents, this can be specified by defining a rewrite rule according to rule [START_REF] Baier | Principles of model checking[END_REF] with an action that is explicitly parallel. A rule specified this way will only rewrite to a legal configuration if concurrent processes manage to synchronize their actions accordingly.

Example 5. (Synchronization) Consider an action t (for transport) that moves a victim to a target position when two agents perform it synchronously. A single agent trying to transport a victim has no effect and should be interpreted as a precondition violation. Thus, this action requires synchronization of agents' actions. This fact is specified as follows (considering a deterministic outcome for the sake of simplicity).

(pos(R, P ) ∧ pos(R , P ) ∧ pos(V, P )) p × t(R, V, P ) t(R , V, P ) → φ(pos(R, P ) ∧ pos(R , P ) ∧ pos(V, P )) p * 1.0 .

If there is need for agents to synchronize, it may be valuable for agents to coordinate their actions by waiting for others to collaborate, eventually rendering a desired action executable. To this end, if an agent should execute an action α as soon as its precondition σ preα is satisfied, waiting for satisfaction of preconditions (e.g. collaborating agents) can be specified in terms of a macro waitFor. Note that σ preα can be determined from the lefthand side of the domain specification rule that specifies the dynamics of α.

waitFor(α) = while ¬σ preα do noop end while ;α .

Probabilistic Model Checking of Action Programs

This section shows how to perform symbolic probabilistic model checking for action programs, whose interpretation results in configurations containing action traces determined through application of Ax-matching and rewriting as shown in section 3. To this end, this section discusses the relation between typical system properties to be model-checked and rewriting of configurations. System properties are expressed in terms of PCTL formulas. For an in-depth discussion of model-checking in general, and model-checking with PCTL in particular, see e.g. [START_REF] Baier | Principles of model checking[END_REF]. For the relation of model-checking and classical planning see e.g. [START_REF] Giunchiglia | Planning as model checking[END_REF].

A typical property that can be checked for an action program is whether it contains a legal trace that will reach a particular goal state satisfying7 a property σ goal within a given number of steps h with at least a desired probability p min . This property can be expressed in terms of a PCTL formula, where P ≥pmin denotes the requirement that its argument is satisfied at least with probability p min , and the eventually operator ♦ ≤h denotes that its argument state is eventually reached within the given horizon h.

P ≥pmin (♦ ≤h σ goal ) (18)
To check whether a given configuration ξ init satisfies this property, a positive reward is specified for states that satisfy σ goal , i.e. R(σ goal ) > 0; all other states expose a reward of zero. Then, (legally terminating) traces eventually satisfying σ goal expose a positive reward.

Ξ + τ ↓ (ξ init ) = {ξ ξ ∈ Ξ τ ↓ (ξ init ) ∧ v ξ (ξ) > 0} (19)
To determine the probability of a trace eventually satisfying σ goal , the probabilities of terminated configurations with equal traces (arising due to nondeterminism) are summed up. If there is no such trace, the probability is zero.

P + ↓ (τ, ξ init ) = ξ∈Ξ + τ ↓ (ξinit) p ξ (ξ) (20)
Property ( 18) is satisfied if there exists a legally terminating trace with an expected value greater than zero and a probability of eventually reaching a state satisfying σ goal greater than p min .8

P ≥pmin (♦ ≤h σ goal ) ⇔ ∃τ ∈ T ↓ (ξ init ) : V e (τ, ξ init ) > 0 ∧ P + ↓ (τ, ξ init ) ≥ p min (21)
In general, a PCTL formula of the form P J (♦ ≤h σ), where J is an interval in [0; 1] can be checked for any initial configuration ξ init ∈ Ξ by specifying a reward greater than zero for states subsumed by σ, and zero reward for all other states; then, it is checked by rewriting whether probabilities of legal traces whose expected value is bigger than zero are in the interval J.

P J (♦ ≤h σ goal ) ⇔ ∃τ ∈ T ↓ (ξ init ) : V e (τ, ξ init ) > 0 ∧ P + ↓ (τ, ξ init ) ∈ J (22)
In particular situations, a system may be required to maintain a particular state property σ maintain . In these cases, it may be valuable to ensure a minimal probability p min that the desired property will sustain with program execution. The PCTL formula P ≥pmin ( ≤h σ maintain ) expresses this system property, where the always operator ≤h denotes that its argument state is always satisfied within the given horizon h. This property can be reformulated in terms of an achieve goal that requires an upper bound on the maximal probability that the desired property will be violated by program execution: P <1-pmin (♦ ≤h ¬σ maintain ). This property can then be checked according to (21). Due to the duality of the always and eventually operators, transformation of maintain to achieve goals can be generalized for probability intervals [START_REF] Baier | Principles of model checking[END_REF].

P ]p,p ] ( ≤h σ) = P [1-p ,1-p[ (♦ ≤h ¬σ) (23)

Example

As a short informal example, consider a rescue scenario. There are two robots r 1 and r 2 at positions p 1 and p 2 , respectively. There are also two victims v 1 and v 2 , the former at position p 1 , the latter at a position p 3 . I.e. σ init := pos(r 1 , p 1 ) ∧ pos(r 2 , p 2 ) ∧ pos(v 1 , p 1 ) ∧ pos(v 2 , p 3 ) (see figure 1). The robots are supposed to transport victims to the safety area; to this end, a reward of one is given if there is any victim at the safety area sa, i.e. R(pos(V, sa)) = 1. Consider the following part of an action program that specifies a behavioural policy for the robots, where actions move and t are defined as in examples 1 and 5. It states that a robot R either moves to the position P of a victim V if there is any, or, if the robot is already at a position of a victim, it waits until it can transport the victim to the safety area in collaboration with another robot.9 policy(R) := while σ do ?(pos(V, P )){move(R, P )}# ?(pos(V, P ) ∧ pos(R, P )){waitFor(t(R, V, sa))} end while

The robots can interpret the action program π := policy(r 1 ) policy(r 2 ) for a σ init , for example for a planning horizon of 2 (because, for example, their energy resources suffice only for this horizon). Interpretation of the program leads to various traces due to the choice operator and due to the non-deterministic effect of move. Rewriting of an initial configuration ξ init := σ init 1.0×0.0 × π × π × 2 will result in a number of configurations, two of which are considered in more detail.

ξ init → ! (pos(r 1 , sa) ∧ pos(r 2 , sa) ∧ pos(v 1 , sa)) 0.9×1.0 × π × τ 1 × 0 ∨ (pos(r 1 , sa) ∧ pos(r 2 , sa) ∧ pos(v 2 , sa)) 0.81×1.0 × π × τ 2 × 0 ∨ ...
where τ 1 = noop move(r 2 , p 1 );t(r 1 , v 1 , sa) t(r 2 , v 1 , sa) τ 2 = move(r 1 , p 3 ) move(r 2 , p 3 );t(r 1 , v 2 , sa) t(r 2 , v 2 , sa) τ 1 is arising from r 1 waiting and r 2 moving successfully to p 1 before they transport v 1 to the safety area, τ 2 represents the trace where both robots successfully move to p 3 and subsequently transport v 2 to the safety area. Figure 1 informally illustrates σ init and the two traces τ 1 and τ 2 . For the robots to decide which choice is more valuable according to reward specification, the traces' expected values can be determined: V e (τ 1 , ξ init ) = 0.9 and V e (τ 2 , ξ init ) = 0.81. Therefore, deciding on τ 1 is the preferable choice of actions in the state σ init .

Expected values and legal termination probabilities can also be used to prove that executing π in σ init satisfies the PCTL property P ≥0.9 (♦ ≤2 pos(V, sa)), as τ 1 ∈ T ↓ (ξ init ) and V e (τ 1 , ξ init ) > 0 ∧ P + ↓ (τ 1 , ξ init ) = 0.9 (see section 4).

Related Work

As mentioned in section 2.2, prominent action programming formalisms have been developed: the situation calculus with its language Golog [8] and the fluent calculus with its language Flux [START_REF] Thielscher | Flux: A logic programming method for reasoning agents[END_REF]. As already outlined, the situation calculus uses regressive fluent-wise specification of dynamics, which contrasts strongly with modern software design where dynamics are typically progressively defined operation-wise. Regarding this issue, the fluent calculus is more close to modern software design paradigms, as is the approach presented in this paper. While there is a decision-theoretic variant of Golog called DT-Golog employing the situation calculus [START_REF] Boutilier | Decision-theoretic, high-level agent programming in the situation calculus[END_REF], and there is a decision-theoretic extension to the fluent calculus (the probabilistic fluent calculus [START_REF] Hölldobler | A logic-based approach to dynamic programming[END_REF]), there is no procedural language exploiting decision-theoretic evaluation for a progressive action calculus, as Flux is purely declarative. The relationship of classical planning and model checking has been investigated thoroughly [START_REF] Giunchiglia | Planning as model checking[END_REF], but, to the best of the author's knowledge, symbolic PCTL model checking approaches have not been investigated in the context of action programming in particular. Both Golog and Flux have been implemented in the Prolog language, where specification of domain theories and action programs is done in terms of a logic program. While this is a reasonable approach for the reasoning tasks tackled by these formalisms, Prolog does not explicitly provide support for formal, algebraic software engineering like Maude [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF][START_REF] Clavel | All About Maude -a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic[END_REF]. Thus, Maude's features like modularization, explicit sort-hierarchies and polymorphism as well as metalanguage operations and user-definable syntax provide additional properties to an action language specified in rewriting logic, as rewrite theories can be implemented in terms of Maude modules straightforwardly. Also, model checking as shown in section 4 is quite naturally supported by a Maude implementation due to its built-in search operator.

Conclusion & Further Work

Conclusion

This paper reports on efforts to integrate various aspects of action programming, algebraic software engineering and model checking to ease the specification of concurrent autonomous systems which expose formally verifiable behaviour and are able to evaluate action alternatives in a decision-theoretic manner, allowing them to autonomously take decisions at runtime that are sensible w.r.t. specified system goals. Domain knowledge (i.e. a relational MDP) is specified as a rewrite theory; system behaviour in terms of a procedural action program. Decisiontheoretic evaluation and model-checking of action programs are performed by matching and rewriting modulo the given rewrite theory. Solutions have been provided for typical problems of symbolically reasoning systems like the frame, projection and legality problems. The approach supports true concurrency in the presence of sharing, and provides facilities to specify synchronization and coordination of actions. Symbolic PCTL model checking of typical system properties has been discussed. Action programming in rewriting logic without support for decision-theoretic concepts has been implemented in the Maude language [START_REF] Belzner | Action programming in rewriting logic[END_REF]. 10

Further Work

Some directions for further work remain. It would be interesting to provide support for situations with incomplete knowledge, where properties of the environment have to be actively sensed. To this end, sensing actions have to be induced to plans, possibly considering sensing costs and expected rewards.

While explicit specification of concurrency has been discussed in this paper, evaluation of concurrent programs is performed centralized. In large-scale multiagent domains it is valuable to decentralize the decision making process by localizing and distributing knowledge. In order to coordinate behaviour, sophisticated communication and interaction models (e.g. scel [START_REF] De Nicola | A language-based approach to autonomic computing[END_REF]) should be integrated with reasoning abilities of agents.

Finally, the relation of action programming and model checking discussed in section 4 only treated a particular class of PCTL formulae. Generalizing this approach as done for classical planning [START_REF] Giunchiglia | Planning as model checking[END_REF] could allow for specification of more complex goals and model checking of more complex system properties.

) Example 3 .

 3 (Action Rules for Concurrent Domains) Consider the specification of actions grab and drop in a domain with concurrency. Note how state properties changed by the actions are locked. (pos(R, P ) ∧ pos(O, P )) p × grab(R, O) → (pos(R, P ) ∧ φ(on(R, O))) p * 0.9 . (pos(R, P ) ∧ pos(O, P )) p × grab(R, O) → (pos(R, P ) ∧ pos(O, P )) p * 0.1 . (pos(R, P ) ∧ on(R, O)) p × drop(R, O) → (pos(R, P ) ∧ φ(pos(O, P ))) p * 1.0 .

Fig. 1 .

 1 Fig. 1. Two traces τ1 and τ2 of executing policy(r1) policy(r2) in state σinit.

Throughout the paper, variables are denoted by uppercase letters.

Maude's built-in search operator performs a breadth-first search; a depth-first strategy can be defined using Maude's internal strategies[START_REF] Clavel | All About Maude -a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic[END_REF] or a dedicated strategy language[START_REF] Eker | Deduction, strategies, and rewriting[END_REF], e.g. by assigning rule application preferences.

Note that partial observable domains can be accounted for by rewriting an initial configuration i (σ i p i ×v i )×π × π ×h with i p i = 1, where the σ i represent different possible states an agent considers, each with probability p i .

For action-wise rewards, it is v := v + R(σ, α , σ1 ∧ σ2). Then, for parallel actions reward is additive: R(σ, α α , σ ) = R(σ, α, σ ) + R(σ, α , σ ).

A state σ satisfies a property σ ? if σ ? σ (see section 3.3).

Depending on the property to be checked, existential quantification is to be replaced by universal quantification.

The loop condition σ will always subsume any state, as it is the identity element for states and subsumption is performed through Ax-matching.

This work has been partially funded by the EU project ASCENS, 257414.