Adorjan Kiss
email: kiss@lirmm.fr

Joël Quinqueton

Learning user preferences in a multiagent system

We present in this paper some attempts to design a Machine Learning method to predict preference knowledge in a multi-agents context. This approach is applied to a corporate knowledge management system.

Introduction

In this paper we will present some attempts to design a Machine Learning method to predict preference knowledge in a multi-agents context. Here we define preference knowledge as knowledge about a preference between elements of a set.

For instance, the documents found by a search engine on the web are ordered according to a preference function computed from the user request. Thus, they can be considered as ordered according to a preference relation.

The framework that gave birth to this work is a joint research project, CoMMA 1 , dedicated to corporate memory management in an intranet. The main objective of the project is to implement and test a Corporate Memory management framework integrating several emerging technologies in order to optimize its maintenance and ease the search inside it and the use of its content by the members of the organization.

The main challenge is to create a coherent system that relies upon several promising new technologies which are in the middle of their struggle to become standards:

-Multi-agent architecture: it is well suited to the heterogeneity of the Corporate Memory; its flexibility eases the system maintenance and keeps the rhythm with the dynamics and evolution of the Corporate Memory; cooperating and adaptive agents assure a better working together with the user in his pursuit to more effectively achieve his goals. The FIPA standard, supported by the CoMMA project, offers the specifications for interoperable intelligent multi-agent systems.

-XML: is a standard recommended by the World Wide Web Consortium intended to offer a human and machine understandable description language: a good choice if it is important to ensure an easy maintenance, and seamless flow through various information processing systems that evolve in time.

-RDF/RDFS another W3C recommendation, that creates a semantic level on the top of XML formal description. RDF annotations allow having an integrated, global view of the Corporate Memory keeping untouched (in terms of storage, maintenance) the heterogeneous and distributed nature of the actual info sources. RDF also allows us to create a common ontology to represent the enterprise model. The ontological commitment, a fundamental choice in our approach to design the Corporate Memory, is motivated by our belief that the community of corporate stakeholders is sharing some common global views of the world that needs to be unified and formalized (RDFS) to form the basis of the entire information system. -Machine Learning Techniques make the system adaptive to the user, and comes even more naturally due to the previous choices, as presented in the following section.

The role of preference in Knowledge Management

The purpose of this section is to discuss how our work (preference learning) fits into the Knowledge Management system.

Getting the user profile

One of the advantages of an enterprise that should be exploited by such a corporate information management system is that the users (i.e. the employees) can be known (their domains of interest/competence, their current activities/tasks). This can be especially useful in some cases where users are likely to be overwhelmed by the quantity of information to process and navigate themselves through (new employees during accommodation, technology monitoring scientists) who would appreciate personalized, automated help in their process of information retrieval.

Using semantic annotations

On the other hand, we have "human and machine understandable" semantic information upon the corporate knowledge offered by the RDF formalization, based upon an "enterprise ontology" (RDF schema). The combination of these two sources of information can provide a rich ground to infer knowledge about the users probable/possible preferences. This combination is made possible due to the fact that we use the same RDF standard for formalizing the user profile; the same base ontology for the enterprise and user models.

It can be imagined that the information combined from these sources will form sets of attributes that will be used as input for a Machine Learning (ML) mechanism.

In order to set up such a ML mechanism, there are two main tasks to carry out:

1. Getting and formalizing the information to be decomposed as attributes to feed the ML mechanism. 2. Defining the ML methodology to process this info

Collecting the information to create a set of most meaningful attributes

We will need to answer the following question: Why does a user prefer a document?

In our attempt to give an example of some possible answers, we are gradually going deeper and deeper into details in case of complex answers: The document is interesting.

-Because it has been stated so:

• By the user himself (the user has already seen the document, and "told" the system, that he is interested in) • By someone else (someone, maybe "close" to the user, wanted to share a favorable opinion about a document) -Because it concerns a topic close to the users interest fields:

• by the relation with the user: * Personal interest fields * Professional interest fields (known by his role in the enterprise) • by the way they are obtained:

* Declared interest fields (the user has stated his interest in documents concerning a topic) * Implied interest fields (the user is included in a community of interest which is close to a topic, like in [START_REF] Pechoucek | Cplant: An acquaintance model based coalition formation multi-agent system[END_REF])

The second question, that introduces the notion of temporality into the preference: Why does a user prefer a document at a given moment?

In other words, to make the difference from the first question: Why does a user prefer a document at a given moment, and does not prefer it at another moment?

The document is interesting only if seen the first time (or the first few times)

-It is interesting during a certain period:

-When the user performs a certain activity -Etc.

These answers are just some samples, one can think of many other possible reasons. Though, it is a very important to find the right questions and answers, that include the majority of possible situations. Indeed, getting the right questions and answers and translating them into quantifiable attributes, and making sure that the highest number of possible situations are observed is a key to the success of such a learning mechanism, that may even outclass in importance the chosen learning technique.

Nevertheless, we will present our approach in the Comma project to choose some typical answers and attributes, but we will focus more on the second issue: the preference learning methodology.

The design of the CoMMA system

The design of CoMMA, presented in this section, can be viewed as our attempt to implement a corporate knowledge management framework.

The agent architecture

The chosen MAS consists of a society of coarse-grained agents, that fulfill in general multiple roles, and are organized in a small number of functional subsocieties. The MAS architecture was designed in order to optimize task-division, flexibility and robustness of the system, and network layout (extensibility, scalability, traffic optimization).

For the implementation of the prototype system, the Jade agent platform was chosen, which is an Open Source Project developed by project partners, University of Parma and CSELT. Jade is an agent platform implemented in Java, which is Fipa compliant, thus having the advantage of a wide opening towards Internet and the Web, interoperability with other MAS-s, and future systems.

In the current status of implementation, the CoMMA system will help the user in three main tasks:

insertion and RDF annotation of documents, search of existing documents, and autonomous document delivery in a push fashion to provide the user with information about new documents that the system predicts interesting for him.

The agent categories present in the system can be classified into four main areas:

1. Document and annotation management. 2. Ontology (Enterprise and User Models) management. 3. User management. 4. Agent interconnection and matchmaking.

The agents from the document dedicated sub-society are concerned with the exploitation of the documents and annotations composing the corporate memory, they will search and retrieve the references matching the query of the user with the help of the ontological agents.

The agents from the ontology dedicated sub-society are concerned with the management of the ontological aspects of the information retrieval activity especially the queries about the hierarchy of concepts and the different views.

The agents from user dedicated sub-society are concerned with the interface, the monitoring, the assistance and the adaptation to the user. Finally the agents from the interconnection dedicated sub-society are in charge of the matchmaking of the other agents based upon their respective needs.

We have already experimented such an architecture in Network Supervision [START_REF] Esfandiari | An interface agent for network supervision[END_REF], with Machine Learning abilities [START_REF] Quinqueton | Chronicle learning and agent oriented techniques for network management and supervision[END_REF]. More recently, an interactionbased strategy has been experimented [START_REF] Sabouret | Learning collective behavior from local interactions[END_REF].

The learning agent

The first context to assess preference learning was chosen to be the document retrieval scenario, via semantic annotations. The search engine used for document retrieval in the CoMMA system is an inference engine called CORESE [START_REF] Corby | A Conceptual Graph Model for W3C Resource Description Framework[END_REF] developed by INRIA, one of the partners of the project. CORESE uses Conceptual Graphs and combines the advantages of using the RDF language for expressing and exchanging metadata, and the query and inference mechanisms available in CG formalism. In order to produce inferences, CORESE exploits the common aspects between CG and RDF: it defined a mapping from annotation statements (RDF triples) to Conceptual Graphs and vice-versa.

One of the shortcomings of such a query retrieval engine is that there is no standard method to sort the information returned, such as keyword frequency in keyword-based search engines. The returned data set must be post-processed, filtered and sorted to present the user with the relevant information. Here comes the aid offered by our ML mechanism.

In the CoMMA system, information that feeds the ML comes from several sources: The document sub-society (the annotations accompanying a query response), the user sub-society (user monitoring and explicit user feedback), and ontology sub-society (to help getting the meaning of the results). Therefore, the learning behavior was awarded to the User Profile Manager agent, which belongs to the connection dedicated sub-society, and performs notably a role of middleman between agents. This decision was justified also by network traffic optimization reasons, especially because in reaction to a user action (query), several interactions can be triggered between agents of different roles.

For example, during a query retrieval, the main interactions are as described in the following figure.

Archivist Archivist

...

User agents

Document agents

UPM Query Processed answer

Identify user Preprocess query: enrich with information from the profile

Post-process answer: Filter, sort using ML prediction Analyze the response: eventually create extra queries to collect more details for the ML Distribute the query between archivists, then collect the answers

Enriched query Answer

The learning cycle

The goal of the ML component is to produce a set of rules that will be used to produce predictions about user preferences. It can be supposed that the system starts with a set of predefined rules, that will be gradually improved during the process of adaptation to users. Otherwise, the system would start with an empty knowledge base, and will undergo a training period, to accumulate sufficient knowledge to allow its deployment.

In our approach, user adaptability comes from both implicit observation of the user (user monitoring subsystem), and explicit user feedback.

Within the ML subsystem, we use a "predict-or-learn" type protocol, that is, when the input is coming from query answers, the system tries to use its knowledge to predict, otherwise, when the input comes from the user in the form of negative feedback, the system tries to update its rules set.

A sample set of attributes

A sample set of attributes is used to create instances from the answers we gave as examples to the question of preference. We tried to make it diverse and for most of them restricted the scope as much as possible for the sake of simplicity of our prototype. We also tried to stick close to the concepts defined in the prototype ontology, that we used as a basis for our first enterprise model.

The first set of attributes relates the document to knowledge recorded in the user profile. Concepts defined in the ontology which are used for this purpose are T opic, Concerns, Interestedby, Communitiesof Interest, etc .

We have also used a number of attributes automatically generated by user monitoring. In our example we have imagined a simple user monitoring scenario, that supposes tracking each consultation of a document by the user, and building a navigation history (or consultation trace). These attributes refer to statistics about document and document category visits.

Finally we have a set of attributes containing specific information about the particular document being analysed (ratings for the document of the user in question, public ratings of other users eventually close to the user).

The issue regarding the correctness of the choice of these concepts, how to make them more generic or how they can be adapted to a specific enterprise, we are addressing in the next stage of our project: there we will intend to create a generic process for attribute collection, instead of analyzing how these attributes are fit for their purpose.

The use of Preference knowledge

As mentioned in the introduction we define preference knowledge as knowledge about a preference between elements of a set. Such knowledge can be stated in various forms: a numerical value assigned for each item, a total ordering relation, a partial ordering relation or even a preordering of the set.

Logical models have been proposed to deal with such knowledge, some dealing directly with the comparison abilities [START_REF] Schobbens | A comparative logic for preferences[END_REF].

It is generally admitted that a preference stands for an order that maybe partial, even a preorder, but that it is often convenient to represent it by a linear extension (which is a total order) or a numeric value compatible with the known orderings.

Then, in terms of Machine Learning, different strategies may be used, depending on the form of the preference knowledge.

Numeric labelling

A numeric labeling, i.e. a mapping of our set of examples into a set of real numbers, is a convenient way to summarize a preference relation. Some Machine Learning methods are available to learn numerical variables [START_REF] Gascuel | A conceptual regression method[END_REF][START_REF] Breiman | Stacked regression[END_REF][START_REF] Breiman | Bagging predictors[END_REF].

Generally, the methods for learning to predict a numerical variable v measure the quality of a predictive rule R by the standard deviation Q(R, v) = σ 2 (v|R) of the value of the variable among the set of objects verifying the concept R to be tested.

The lower Q(R, v) is, the better R is to predict v, because the mean value of v can be used with less error. With such criteria, any learning method will lead to grouping several neighbour values around their mean. Then, the learnt rules will not be very different from rules learnt from examples roughly rated with a finite set of values.

The order relation

By definition, a binary relation, which we note , is an order if it has the following properties:

reflexive x x, transitive: if x y and y z, then x z, antisymmetric: if x y and y x, then x = y.

Then, we can imagine to learn the binary relation by learning each of its elements, that is, learn on each couple of objects (a, b) such that a b. Then, let us summarize the suitable properties of such a learning set for this approach to work correctly.

First, if (a, b) with a b is an example, then (b, a) is a counter-example. Then, what happens to (a, a)? We can see that they would be both examples and counter-examples, then it is better to consider the strict order relation, and eliminate diagonal elements.

With these hypotheses, the description of an example is made of 2 parts: the attributes which are modified between a and b, and those which keep the same value. We can notice here that these attributes are the same as those involved in the sorting tree of our examples.

Finally, our method appears to be "half lazy", in comparison with lazy learning methods, like kNN or LWR [START_REF] Aha | Tolerating noisy, irrelevant, and novel attributes in instancebased learning algorithms[END_REF]. Our learned knowledge is partly explicit, but in the classification step, we need to compare a new instance with several elements of the learning set (maybe in a dichotomic way) to put it in the right place.

Statistical evaluation criteria

Usually in Machine Learning, particularly for building of decision trees, the learned classification rules are evaluated by their similarity to the desired classification.

We can use the same principle here, and we have two possible families of criteria. If we can compute a rank for each element, the similarity is computed by measuring the rank correlation to the expected ranking. Otherwise, each pair must be given: then we use a pairwise comparison between the expected order and the learnt order.

Several measures of similatity between 2 different orderings of the same data have been proposed. In each case, one has to deal with tied elements.

The Spearman rank order correlation The Spearman rank order correlation r s is a correlational measure that is used when both variables are ordinal. The traditional formula for calculating the Spearman rank-order correlation is

Corr(r, r ) = 1 - 6 i=n i=1 (r i -r i ) 2 n(n 2 -1)
where r and r are the ranks to compare of paired ranks. When there are tied cases they should be assigned the mean of their ranks. The mean of the ranks from p+1 to p+n is

1 n ( (n+p)(n+p+1) 2 -p(p+1)
2

), which become after simplification n+2p+1 2

.

The Kendall pairwise τ criterion When we have to compare each pair of data, they can be classified as either tied (T), concordant (P), or discordant (Q).

The best measure for this case is Kendall's τ b which takes into account a correction for tied pairs. Its formula is

τ b = P -Q (P + Q + T x )(P + Q + T y )
where T x is the number of pairs tied on X but not Y, and T y is the number of pairs tied on Y but not X.

Verifying the consistency of the method

In the case we perform a pairwise learning of the order relation, we can notice that a fundamental property, the transitivity, can be guaranteed by the learning process itself, as we show below for a version space method [START_REF] Mitchell | Machine Learning[END_REF].

We can check that, if, for 3 examples the transitivity holds, then it is not necessary to add the 3rd pair as example to learn the relation : Of course, this is only a scheme of the proof, and is, strictly speaking, only available for version-space-like learning. In a more general case, like decision tree learning, we can only make the hypothesis that it is true. We concluded that we could learn directly a sorting rule (in a greedy way, like decision trees) and evaluate the obtained rule with the τ criteria defined in section4.3.

Conclusion

The Machine Learning and user adaptability component is a very important aspect in the CoMMA project. In this paper we presented the advances that we have made in this domain, especially focussing on the learning of preference data for document retrieval.

The main choice we focus on does not only present the usefulness of Machine Learning, but also tries to overcome some of the gaps and limitations of semantic based information retrieval systems.

The first implementation of our algorithm has given the expected quick results during the intermediate trials during the project, and allowed experimental validation through feedback from the users. The next stage of our research is focusing on the "generic lerning problem", that instead of being built upon a predefined set of attributes, will try to offer a formal procedure to collect the attributes from "observable concepts" present in the ontology.

Fig. 1 .

 1 Fig. 1. The main interactions in CoMMA during a query

-

  let (a, b) = (a 1 . . . a n , b 1 . . . b n ) and (b, c) = (b 1 . . . b n , c 1 . . . c n ). Then, S is of the form L ∧ R, with the left part L as a generalisation of both a and b, and the right part R of both b and c. Then, as L is a generalisation of a and R of c, S is a generalisation of (a, c). with the same conventions, G has a disjunctive form whose elements reject all the examples, then, if we represent any of its elements as L ∧ R. If (b,a) and (c,b) are rejected, it means that L rejects b or R rejects a, and L rejects c or R rejects b. But G must also be a generalisation of S.

1 This work was supported by the CoMMA (Corporate Memory Management through Agents) project [Con00] funded by the European Commission under Grant IST-1999-12217, which started beginning of February 2000.


Alain Finkel
email: alain.finkel@ens-paris-saclay.fr

Ekanshdeep Gupta
email: umirelaxekanshdeep@cmi.ac.in

The Well Structured Problem for Presburger Counter Machines

Keywords: 2012 ACM Subject Classification Theory of computation Well structured transition systems, infinite state systems, Presburger counter machines, reachability, coverability

We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.

Introduction

Context: Well Structured Transition Systems (WSTS) [START_REF] Finkel | Reduction and covering of infinite reachability trees[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF] are a well-known model to solve termination, boundedness, control-state reachability and coverability problems. It is well known that Petri nets and Vector Addition Systems with States (VASS) are WSTS and that Minsky machines are not WSTS. But the characterization of counter machines which are well structured (resp. with strong monotony) is surprisingly unknown. Moreover, given a counter machine, can we decide whether it is well structured (resp. with strong monotony)? These questions are relevant since a positive answer could allow to verify particular instances of undecidable models like Minsky machines and counter machines. In this paper, we consider Presburger counter machines (PCM) where each transition between two control-states is labelled by a Presburger formula which describes how each counter is modified by the firing of the transition. The PCM model includes Petri nets, Minsky machines and most of the counter machine models studied in the literature, for example counter machines where transitions between control-states are given by affine functions having Presburger domains [START_REF] Boigelot | Symbolic verification with periodic sets[END_REF][START_REF] Finkel | How to compose presburger-accelerations: Applications to broadcast protocols[END_REF].

Affine VASS: In an Affine VASS (AVASS), transitions between control-states are labelled by affine functions whose matrices have elements in Z (and not in N as usual). AVASS extends VASS (where transitions are translations) and positive affine VASS (introduced as self-modified nets in [22] and studied as affine well structured nets in [START_REF] Finkel | A well-structured framework for analysing Petri net extensions[END_REF]. [START_REF] Bonnet | Extending the rackoff technique to affine nets[END_REF] extends the Rackoff technique to AVASS where all matrices are larger than the identity matrix: for this subclass, coverability and boundedness are shown in EXPSPACE. The variation of VASS which may go below 0, called Z-VASS, is studied in [START_REF] Haase | Integer vector addition systems with states[END_REF] and for their extension, Z-Affine VASS, reachability is shown NP-complete for VASS with resets, PSPACE-complete for VASS with transfers and undecidable in general [START_REF] Blondin | The complexity of reachability in affine vector addition systems with states[END_REF][START_REF] Blondin | Affine extensions of integer vector addition systems with states[END_REF]; let us remark that all Z-Affine VASS have positive matrices. Moreover AVASS allow the simulation of the zero-test so they are at least as expressive as Minsky machines. But for dimension one, AVASS are more expressive than Minsky machines: in fact, P ost * is computable as a Presburger formula for 1-counter Minsky machines but this is not the case for 1-AVASS which can generate the set of all the powers of 2 (this set is not the solution of any Presburger formula).

The computation of the set P re * of all predecessors of a configuration is effective for 2-VASS (extended with one zero-test and resets) [START_REF] Finkel | Reachability for two-counter machines with one test and one reset[END_REF] as a Presburger formula and for pushdown automata [START_REF] Bouajjani | An efficient automata approach to some problems on contextfree grammars[END_REF] as a regular language. But the computation of P re * fails for 3-VASS and for Pushdown VAS since P re * is neither semilinear nor regular [19].

Our contributions:

We introduce two new problems related to well structured systems and Presburger counter machines. The so-called well structured problem: [START_REF] Blondin | Affine extensions of integer vector addition systems with states[END_REF] given a PCM, is it a WSTS? and the strong well structured problem: [START_REF] Blondin | The complexity of reachability in affine vector addition systems with states[END_REF] given a PCM, is it a WSTS with strong monotony?

We prove that the well structured problem is undecidable for PCM even if restricted to dimension one (1-PCM) with just Presburger functions (i.e. piecewise affine functions); undecidability is also verified for Affine VASS in dimension two (2-Affine VASS). The undecidability proofs use the fact that Minsky machines can be simulated by both 1-PCM and 2-Affine VASS. However, we prove the decidability of the well structured problem for 1-Affine VASS (which subsumes 1-Minsky machines). Since the strong monotony can be expressed as a Presburger formula, the strong well structured problem is decidable for all PCMs. These results are summarised below: We give an algorithm that computes P re * of a 1-AVASS and this extends a similar known result for 1-Minsky machines and 1-VASS (and for pushdown automata [START_REF] Bouajjani | An efficient automata approach to some problems on contextfree grammars[END_REF]). The computation of P re * allows us to give a simple proof that reachability and coverability are decidable for 1-AVASS (in fact reachability is known to be PSPACE-complete for polynomial one-register machines [START_REF] Finkel | Reachability in register machines with polynomial updates[END_REF] which contains 1-AVASS). Moreover, the computation of P re * allows to decide the well structured problem for 1-AVASS. These results are summarised below:

Outline: We introduce in Section 2 two models, well structured transition systems (WSTS) and Presburger counter machines (PCM); we show that the property for an ordering to be well is undecidable. Section 3 analyses the decidability of the well structured problems for many classes of PCM and Affine VASS. Section 4 studies the decidability of reachability and coverability for the classes studied in Section 3.

Counter machines and WSTS

A relation ≤ on a set E is a quasi ordering if it is reflexive and transitive; it is an ordering if moreover ≤ is antisymetric. A quasi ordering ≤ on E is a well quasi ordering (wqo) if for all infinite sequences of elements of E, (e i ) i∈N , there exists two indices i < j such that e i ≤ e j . For an ordered set (E, ≤) and a subset X ⊆ E, the upward closure of X denoted by ↑X is defined as follows:

↑X = {x | ∃y ∈ X such that y ≤ x}. X is said to be upward closed if X = ↑X.

Arithmetic counter machines

A d-dim arithmetic counter machine (short, d-arithmetic counter machine or an arithmetic counter machine) is a tuple M = (Q, Φ, →) where Q is a finite set of control-states, Φ is a set of logical formulae with 2d free variables x 1 , ..., x d , x ′ 1 , ..., x ′ d and →⊆ Q × Φ × Q is the transition relation between control-states. We can also without loss of generality assume that → covers Φ, i.e. Φ does not have unnecessary formulae. A configuration of M refers to an element of Q × N d . The operational semantics of a d-arithmetic counter machine M is a transition system

S M = (Q × N d , →) where →⊆ (Q × N d ) × (Q × N d ) is
the transition relation between configurations. For a transition (q, φ, q ′ ) in M , we have a transition (q; x 1 , ..., x d ) → (q ′ ; x ′ 1 , ..., x ′ d ) in S M iff φ(x 1 , ..., x d , x ′ 1 , ..., x ′ d ) holds. Note that we are slightly abusing notation by using the same → for both M and S M . We may omit Φ from the definition of a counter machine if it is clear from context.

A d-dim arithmetic counter machine M with initial configuration c 0 is defined by the tuple M = (Q, Φ, →, c 0 ) where (Q, Φ, →) is a d-arithmetic counter machine and c 0 ∈ Q × N d is the initial configuration. An arithmetic counter machine is effective if the transition relation is decidable (there is a decidable procedure to determine if there is a transition x → y between any two configurations x, y) and this is the case when it is given by an algorithm, a recursive relation, or decidable first order formulae (for instance Presburger formulae). An arithmetic counter machine is said to be functional if each formula in Φ that labels a transition in M defines a partial function.

Most usual counter machines can be expressed with Presburger formulae. It is well known that Presburger arithmetic with congruence relations without quantifiers is equivalent in expressive power to standard Presburger arithmetic [START_REF] Haase | A survival guide to presburger arithmetic[END_REF].

◮ Definition 1. A Presburger counter machine (PCM) is an arithmetic counter machine M = (Q, Φ, →) such that Φ is a set of Presburger formulae with congruence relations without quantifiers.

◮ Proposition 2. [START_REF] Demri | Model-checking ctl* over flat presburger counter systems[END_REF] (proof in Appendix) The property for a d-dim PCM to be functional is decidable in NP.

Minsky machines with d counters are d-PCM M = (Q, Φ, →) where Φ consists of either translations with upwards closed guards, or formulae of the form ∧ d i=1 (x i = x ′ i ) ∧ x k = 0 for varying k (zero-tests). Vector Addition Systems with States (VASS) are Minsky machines q 1 q 2

x ′ = x -13 A positive AVASS S is an AVASS such that every matrix A i of S is positive. This model has been studied for instance in [START_REF] Finkel | A well-structured framework for analysing Petri net extensions[END_REF]. A totallypositive AVASS S is a positive AVASS such that every vector b i of S is positive. For totally positive AVASS, an instance of the boundedness problem has been shown decidable in [START_REF] Finkel | A well-structured framework for analysing Petri net extensions[END_REF].

x ′ = 19 -x x ′ = x -3 x ′ = x
Note that we say something is positive if it is greater than or equal to 0, not strictly greater than 0.

◮ Example 3. The machine M 1 in Figure 1 is a 1-AVASS but it is not a 1-VASS because there is a negative transition from q 1 to q 1 . ◮ Proposition 4. [START_REF] Demri | Model-checking ctl* over flat presburger counter systems[END_REF] Checking whether a given PCM is a VASS, AVASS, positive AVASS or a totally positive AVASS is decidable.

Well structured transition systems

A transition system is a tuple S = (X, →) where X is a (potentially infinite) set of configurations and →⊆ X × X is the transition relation between configurations. We denote by * -→ the reflexive and transitive closure of -→. For a subset S ⊆ X, we denote by P re(S) := {t | t → s for some s ∈ S}, and P re * (S) := {t | t * -→ s for some s ∈ S}. Similarly for P ost(S) and P ost * (S).

An ordered transition system S = (X, →, ≤) is a transition system (X, →) with a quasiordering ≤ on X. Given two configurations x, y ∈ X, x is said to cover y if there exists a configuration y ′ ≥ y such that x * -→ y ′ . An ordered transition system S = (X, →, ≤) is monotone, if for all configurations s, t, s ′ ∈ X such that s → t, s ′ ≥ s implies that s ′ covers t. S is strongly monotone if for all configurations s, t, s ′ ∈ X such that s → t, s ′ ≥ s implies that there exists t ′ ≥ t such that s ′ → t ′ . ◮ Definition 5. [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] A well structured transition system (WSTS) is an ordered transition system S = (X, →, ≤) such that (X, ≤) is a wqo and S is monotone.

The coverability problem is to determine, given two configurations s and t, whether there exists a configuration t ′ such that s * -→ t ′ ≥ t (s covers t). This problem is one often studied alongside well-structuredness.

Let us consider the usual wqo ≤ on Q × N d associated with a d-counter machine M = (Q, →): (q 1 ; x 1 , x 2 , ..., x d ) ≤ (q 2 ; y 1 , ..., y d ) ⇐⇒ (q 1 = q 2 ) ∧ (∧ d i=1 x i ≤ y i ).

We say that an arithmetic counter machine M = (Q, Φ, →) is well structured (or is a WSTS) iff its associated transition system S M is a WSTS under the usual ordering. Since the usual ordering on (Q × N d , ≤) is a wqo, let us remark that the associated ordered transition system

S M = (Q × N d , →, ≤) is a WSTS iff S M is monotone.
Given a counter machine M = (Q, →), the control-state reachability problem is that given a configuration (q; n 1 , ..., n d ), and a control-state q ′ whether there exist values of counters (m 1 , ..., m d ) such that (q; n 1 , ..., n d ) * -→ (q ′ ; m 1 , ..., m d ). In this case, we often say that q ′ is reachable from (q; n 1 , ..., n d ).

We introduce two new problems related to WSTS and Presburger counter machines.

The well structured problem: given a PCM, is it a WSTS?

The strong well structured problem: given a PCM, is it a WSTS with strong monotony?

◮ Example 6. The machine M 1 (Figure 1) is not strongly monotone since we have: (q 1 , 0)

x ′ =19-x
------→ (q 1 , 19). However, we see that P ost * (q 1 , 10) = {(q 1 , 9), (q 1 , 10)}. Therefore we can deduce that (q 1 , 10) cannot cover (q 1 , 19). Hence M 1 is not well structured. We give, in Section 4, an algorithm for deciding whether a 1-AVASS is well structured.

It is shown in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] that almost every transition system can be turned into a WSTS for the termination ordering which is not, in general, decidable. So the problem is not only to decide whether a system is a WSTS in general; we have to choose a decidable ordering. We show that deciding whether arbitrary (non-effective) transition systems are well-structured for the usual (decidable) ordering on natural numbers is undecidable.

◮ Proposition 7. (proof in Appendix) The well structured problem for 1-arithmetic counter machines is undecidable.

We now show that restricting to effective transition systems does not allow us to decide the property of being a WSTS.

◮ Corollary 8. The well structured problem (for the usual ordering on N) for effective transition systems whose set of configurations is included in N is undecidable.

Proof. There exists a reduction from the Halting Problem as follows:

Given a Turing machine M , we define a transition system S M = (N, → M ) as follows: If (m = 0) ∨ (M does not halt in m steps), then, for all n, there is a transition m → M n. Hence this transition relation → M is decidable. Now, if M does not halt, then there is a transition m → M n for all m, n ∈ N. This satisfies monotony, hence in this case, S M is a WSTS. However, if M halts in exactly m steps, then there is no transition from m + 1 but there is, in any case, a transition from 0 to n for all n. Hence in this case, S M is not a WSTS. Therefore, S M is a WSTS iff T does not halt. ◭

Testing whether an ordering is well

In the previous results, the usual well ordering on natural numbers is not necessarily the unique decidable ordering when considering the well structured problem for counter machines.

Let ≤ be a decidable quasi ordering relation on N d . If we are interested in whether a counter machine with this ordering is WSTS, it raises the natural question of whether we can decide if ≤ is a wqo. Unfortunately, but unsurprisingly, we first show that this property is undecidable in dimension one (d = 1).

◮ Proposition 9. (proof in Appendix)

The property for a decidable ordering on N to be a well ordering is undecidable.

Let us study the case of Presburger-definable orderings in N. Among many equivalent characterizations of wqo, we know that a quasi ordering is well iff it satisfies well-foundedness and the finite anti-chain property. Both of these properties can be expressed using monadic second order variables. But, it is shown in [17] that Presburger Arithmetic with a single monadic variable becomes undecidable. Hence, this cannot directly be used to check if a Presburger-definable ordering is a wqo. However, we still have the following result: ◮ Proposition 10. (proof in Appendix) The property for a Presburger relation on N to be a well quasi ordering is decidable.

3

The well structured problem for PCM

In the sequel, whenever we talk about PCM being WSTS, we will consider the usual ordering on Q×N d defined in subsection 2.2. We introduce a general technique to prove undecidability of checking whether a counter machine of some class is a WSTS. Let S 0 be the class of machines we are interested in. We will show reduction from reachability in Minsky machines.

◮ Lemma 11. Suppose we have a procedure which takes a 2 counter Minsky machine with initial state M = (Q, →, q 0 ) and a control-state q 1 as input and generates a machine N of class S 0 which satisfies the following two requirements:

All control-states in M are reachable implies N is a WSTS. (1) N is a WSTS implies q 1 is reachable in M from (q 0 ; 0, 0). (2)
Then, the well structured problem for S 0 is undecidable.

Proof. Suppose that the well structured problem for S 0 is decidable. We will use the above procedure to get an algorithm for Minsky machine reachability. Fix (M, q 1 ), where M = (Q, → M , q 0 ). We want to check if q 1 is reachable from (q 0 ; 0, 0).

Let |Q| = n. Consider all 2 n-2 subsets Q ′ ⊆ Q satisfying that {q 0 , q 1 } ⊆ Q ′ . For each such Q ′ , let → Q ′ denote the restriction of → M to the set Q ′ × Q ′ . Hence, we can associate a Minsky machine M ′ = (Q ′ , → Q ′ , q 0 ) to each such subset Q ′ . We call M ′ a sub-machine of M corresponding to Q ′ .
Now, for each sub-machine M ′ , we consider the machine N ′ of class S 0 , generated by the given procedure from (M ′ , q 1 ). If there exists M ′ such that N ′ is a WSTS, then we have that q 1 is reachable in M ′ (by condition (2)), hence in M .

On the other hand, if q 1 was reachable in M , then let Q reach ⊆ Q be the set of all control-states of M which are reachable from (q 0 ; 0, 0). Let its corresponding sub-machine be M ′ . Since all control-states of M ′ are reachable (by choice of Q reach ), therefore the corresponding N ′ will be a WSTS (by condition (1)).

Hence, q 1 is reachable in M from (q 0 ; 0, 0) iff there exists a subset Q ′ ⊆ Q satisfying that {q 0 , q 1 } ⊆ Q ′ such that the corresponding sub-machine M ′ is a WSTS. Since there are only 2 n-2 such subsets, we can check all of them to decide whether q 1 is reachable in M .

Hence, we have given an algorithm to check reachability in Minsky machine. Therefore, the well structured problem for S 0 is undecidable. ◭

We will use Lemma 11 to prove that the well structured problem for functional 1-dim PCMs is undecidable. To apply Lemma 11, we need to give an algorithm which takes a Minsky machine M = (Q, → M , q 0 ) and a control-state q 1 , and generates a functional 1-dim PCM N 1 satisfying conditions (1) and [START_REF] Blondin | The complexity of reachability in affine vector addition systems with states[END_REF].

Construction of a functional 1-dim PCM N 1 :

Let (M, q 0 ) be given. The procedure to generate a 1-dim PCM N 1 is as follows:

Let v p (n) denote the largest power of p dividing n. For M = (Q, → M , q 0 ), we define the 1-PCM N 1 = (Q, → N , (q 0 , 1)) with the same set Q of control-states. We will represent the values of the two counters (m, n) by the one-counter values 2 m 3 n c for any c such that v 2 (c) = v 3 (c) = 0. Conversely, a configuration (q, n) of N 1 will correspond to (q; v 2 (n), v 3 (n)) of M . Note that, we are allowing multiplication by constants c in N 1 as long as v 2 (n) and v 3 (n) remain unchanged.

Increment/decrement of counters corresponds to multiplication/division by 2 and 3 which is Presburger expressible. Similarly, zero-test corresponds to checking divisibility by 2 and 3 which is again Presburger-expressible. So first, for each transition in → M , we add the corresponding transition to → N . Now, to get the suitable properties of conditions ( 1) and ( 2), we will add two more types of transitions to → N . For each control-state q, we add a transition (q, x ′ 1 = 6x 1 + 1, q 0 ) to → N . We shall call it a "reset-transition" because v 2 (6x 1 + 1) = v 3 (6x 1 + 1) = 0, so this transition corresponds to a counter-reset in M from anywhere regardless of our present configuration. Note that such a transition would not change the reachability set in M . This "reset-transition" is crucial in forcing well-structuredness in N . Also, we add a transition (q 0 , (x 1 = 0 ∧ x ′ 1 = 0), q 1 ) to → N to ensure condition (2). Since the configuration (q 0 , 0) cannot be reached from the initial configuration (q 0 , 1) during any run of N 1 , this will also not affect the reachability set of N 1 . Note that, all of our transitions are functional, hence N 1 is a functional 1-dim PCM. Now, we show that the construction of N 1 satisfies conditions ( 1) and ( 2).

◮ Lemma 12. The functional 1-dim PCM N 1 satisfies condition [START_REF] Blondin | Affine extensions of integer vector addition systems with states[END_REF].

Proof. Suppose that all control-states of M are reachable from (q 0 ; 0, 0). Then we claim that N 1 will be a WSTS. Suppose there is a transition (q, n) → N (q ′ , m) and (q, n ′ ) is a configuration with (q, n ′ ) ≥ (q, n). Hence we want to show existence of some path (q, n ′ ) * -→ N (q ′ , m ′ ) ≥ (q ′ , m).

Case 1: The transition (q, n) → N (q ′ , m) is a "reset-transition". Hence q ′ = q 0 and m = 6n + 1. In this case, note that since n ′ ≥ n, the transition (q, n ′ ) → N (q 0 , 6n ′ + 1) ≥ (q 0 , m) satisfies the requirement. Case 2: The transition (q, n) → N (q ′ , m) is not a "reset-transition". In this case, m ≤ 3n because the above transition corresponds, in M to an increment/decrement in c 1 or c 2 or a zero-test. In each case, we can check that m ≤ 3n. Let there be a path (q 0 ; 0, 0) * -→ M (q ′ ; n 1 , n 2 ) in M for some n 1 , n 2 . Such a path exists because all control-states in M are reachable. Hence, we take the "reset-transition" (q, n ′ ) → N (q 0 , 6n ′ + 1) and follow the corresponding path (q 0 , 6n ′ + 1) * -→ N (q ′ , 2 n1 3 n2 (6n ′ + 1)) ≥ (q ′ , 3n) ≥ (q ′ , m). Hence we have again shown monotony to prove that N 1 is a WSTS.

Hence we have shown that if all control-states of M are reachable, then N 1 is monotone. ◭ ◮ Lemma 13. The functional 1-dim PCM N 1 satisfies condition [START_REF] Blondin | The complexity of reachability in affine vector addition systems with states[END_REF].

Proof. Since there is a transition (q 0 , 0) → N (q 1 , 0), we deduce that if N 1 is a WSTS, then (q 0 , 1) * -→ N (q 1 , n) for some n by monotony because (q 0 , 0) ≤ (q 0 , 1). Also note that since N 1 simulates M , hence reachability of q 1 in N 1 implies that q 1 is reachable from (q 0 ; 0, 0) in M . ◭

Since we have provided a construction of functional 1-dim PCM N 1 satisfying conditions (1) and ( 2), from Lemma 11 we have that:

◮ Theorem 14. The well structured problem for functional 1-dim PCMs is undecidable.

Similarly, we can use Lemma 11 to show this result for 2 counter Minsky machines. This construction is done in the Appendix due to lack of space.

◮ Theorem 15. (proof in Appendix) The well structured problem for 2-dim Minsky machines is undecidable. Now, we make the observation that we can perform zero-tests using affine functions. The basic idea is that a transition x ′ = -x is only satisfied by a counter whose value is 0. Increments/decrements can already be implemented in

x i ≤ y i ) ∧ φ(x 1 , ..., x d , x ′ 1 , ..., x ′ d ) =⇒ (∃y ′ 1 ...∃y ′ d ( d i=1 x ′ i ≤ y ′ i ) ∧ φ(y 1 , ..., y d , y ′ 1 , ..., y ′ d ))))
Since Presburger arithmetic is decidable, the strong well structured problem for d-PCM is decidable.

◮ Remark 17. The validity of the formula of strong monotony can also be decided for extended PCM defined in decidable extensions of Presburger Arithmetic.

4

Decidability results for 1-AVASS Now, let us look at some reachability and coverability results for the various models of AVASS. First, we can simulate 2-counter Minsky machines with 2-AVASS. Since coverability and reachability are undecidable for 2-counter Minsky machines, we directly have the following result:

◮ Corollary 18. Control-state reachability, hence coverability is undecidable for 2-AVASS.

Similarly, we showed in Construction of functional 1-PCM N 1 that we can also simulate 2-counter Minsky machines with functional 1-PCM. Hence, we also have the following: ◮ Corollary 19. Control-state reachability, hence coverability is undecidable for functional 1-PCM. Now, let us examine the case of 1-AVASS. For 1-AVASS, reachability and consequently coverability is decidable from work done in [START_REF] Finkel | Reachability in register machines with polynomial updates[END_REF]. We show that checking whether it is a WSTS is also decidable. Moreover, we give a simpler proof of decidability of reachability and coverability.

Given M = (Q, →) a 1-AVASS and a final configuration (q f , n f ) that we want to check reachability for, we present Algorithm 1 which computes P re * (q f , n f ) as a Presburger formula. A transition (q, x ′ = ax + b, q ′ ) is positive if a ≥ 0. Let a cycle/path in M be called positive if all transitions are positive. A cycle (q 1 , ..., q k , q 1 ) is called a simple cycle if q 1 , ..., q k are all pairwise distinct.

Let us denote by P re q the set P re * (q f , n f ) ∩ ({q} × N). For a transition t = (q, x ′ = ax + b, q ′ ) and a given subset of X ⊆ N, let P re t (X) denote {n : an + b ∈ X}. For a simple cycle c rooted at q with an effective guard and transition, extend the above notation P re c i (X) for i repetitions of the cycle. Then, let P re c * (X) := ∪ i∈N P re c i (X). We will conveniently replace X by a formula which denotes a subset of N.

Algorithm 1 Algorithm for computing

P re * (q f , n f ) in 1-AVASS 1: procedure computePre* 2:
for all q ∈ Q do 3:

φ q ≡ ⊥ 4: φ q f ≡ (n = n f ) 5: for all q ∈ Q do 6:
for all simple cycles c rooted at q do for all q ∈ Q do 13:

φ ′ = φ q 14:
for all transitions t = (q, x ′ = ax + b, q ′ ) ∈→ do 15:

ExploreTransition(t)

16:

for all simple cycles c containing q do 17:

ExploreCycle(c) 18: if φ ′ = φ q then
⊲ Check equality as Presburger formulae

19:

notFinished = True

The algorithm will keep a variable φ q for each control-state q ∈ Q which will store a Presburger formula (with one free variable n) denoting the currently discovered subset of P re q . Let this be denoted by φ q , i.e. φ q := {n : φ q (n)}. For uniformity, we can assume that φ q is a disjunction of formulae of form range ∧ mod where range ≡ (r ≤ n ≤ s) (s possibly ∞) and mod ≡ (n = dq d).

We initially simplify each simple cycle into a meta-transition which is the composition of all individual transitions in the cycle. We will also compute the guard of a cycle. Since each positive transition has an upward closed guard and each negative transition has a downward closed guard, the guard of a cycle will be of the form r ≤ n ≤ s for some r, s ∈ N (s possibly ∞). Hence, we will only consider a cycle in terms of its guard and its meta-transition.

We use two main procedures in computePre*:

1. ExploreTransition: Given a transition t = (q, x ′ = ax + b, q ′ ), it computes P re t (φ q ′ ) and appends it to φ q . 2. ExploreCycle: Given a simple cycle c rooted at q, it computes P re c * (φ q ) and appends it to φ q .

◮ Lemma 20. (proof in Appendix) For any transition t, and any simple cycle c, given φ q , P re t (φ q ) and P re c * (φ q ) are both Presburger expressible and effectively computable.

With this lemma the algorithm is well-defined. Now let us prove the termination and the correctness of the algorithm.

◮ Proposition 21. Algorithm computePre* terminates.

Proof. For each q, we will show that P re q can be obtained in finitely many iterations of the algorithm. Let q ∈ Q be arbitrary.

Case 1: P re q is finite: Each value will be discovered in finitely many iterations, hence P re q will be obtained in finitely many iterations. Case 2: P re q is infinite: Since we are talking about reaching (q f , n f ), we note that the only transitions which can decrease arbitrarily large values are transitions of the form x ′ = b or x ′ = x -a, a > 0. Hence, since P re q has arbitrarily large values, and each run has to reach n f (i.e. has to be decreased), we can see that there must either be a transition x ′ = b, or a positive cycle with meta-transition x ′ = x -a, reachable from q through a positive path.

Case 2.i:

There is a transition x ′ = b: In this case, there exists N such that for all n ≥ N , the same path suffices. In this case, once the aforementioned path is discovered, {n : n ≥ N } becomes a subset of φ q ⊆ P re q , which leaves finitely many values in P re q \ φ q , which can again be discovered by finitely many additional runs. Case 2.ii: There are positive cycles with meta-transition x ′ = x -a:

The idea is that we will cover P re q when we compute P re c * for such a cycle c. This is because for such a cycle, all that matters is the value of the counter modulo a. Since there are only finitely many distinct values modulo a, these will again be discovered in finitely many runs. Hence, each cycle will be discovered in finitely many runs. Therefore since there are finitely many simple cycles, the corresponding values of P re q will also be discovered in finitely many runs.

Hence, for all q, in finitely many runs we will get P re q = φ q . At such a point, the algorithm has to stop, hence termination is guaranteed. ◭ ◮ Theorem 22. (Correctness) Given a 1-AVASS M = (Q, →) and a configuration (q, n), the algorithm computePre* computes P re * (q, n) as a Presburger formula.

Proof. We will show that Algorithm 1 upon termination will always have φ q = P re q . That φ q ⊆ P re q should be clear. Suppose the algorithm terminates with φ q P re q for some q ∈ Q. For some value n ∈ P re q \ φ q , consider a path which covers (q 2 , n 2 ), say the path is (q, n) → (p 1 , n 1 ) → ... → (p m , n m ) → (q 2 , n ′ ). In such a path, consider the largest i, such that n i / ∈ φ pi . Now, in the last iteration of the algorithm, since n i+1 ∈ φ pi+1 (by choice of i), hence, we will explore the edge to include n i ∈ φ pi . Hence, the algorithm would not have terminated. Contradiction. Hence, when the algorithm terminates, φ q = P re q . ◭ ◮ Example 23. Let us consider machine M 1 in Figure 1. Suppose we want to compute P re * (q 1 , 19). We begin with φ q1 ≡ (n = 19), φ q2 ≡ ⊥. If we apply ExploreTransition to the transition (q 2 , (x ′ = x), q 1 ), we will get φ q2 ≡ (n = 19). If we now apply ExploreCycle to the cycle (q 2 , x ′ = x -3, q 2 ), we will get φ q2 ≡ (n ≥ 19 ∧ n = 3 1). Continuing like this, we end up with φ q1 ≡ (n ∈ {0, 3, 6, 19}∨(n

≥ 13∧n = 3 1)∨(n ≥ 32∧n = 3 2)∨(n ≥ 45∧n = 3 0)) and φ q2 ≡ (n ≥ 0 ∧ n = 3 0) ∨ (n ≥ 19 ∧ n = 3 1) ∨ (n ≥ 32 ∧ n = 3 2
). This is P re * (q 1 , 19).

◮ Corollary 24. (proof in Appendix) [START_REF] Finkel | Reachability in register machines with polynomial updates[END_REF] Reachability (hence coverability and control-state reachability) for 1-AVASS is decidable.

◮ Remark 25. Algorithm 1 also works if we extend the model of 1-AVASS with Presburger guards at each transition. Hence, reachability, coverability and the well-structured problem are all decidable for this model as well.

It could be useful to determine whether an 1-AVASS is a WSTS (with strict monotony) because if it is the case, it will allow to decide other problems like the boundedness problem that is not immediately a consequence of the computability of P re * (↑(q, n)). Since we can compute P re * (q, n), we can also compute P re * (↑(q, n)) by the same technique as in Corollary 24 (check Appendix). This can be used to determine whether a given 1-AVASS is a WSTS as follows.

◮ Theorem 26. The well structured problem is decidable for 1-AVASS.

Proof. First we show that M is a WSTS, iff for all negative transitions (q 1 , (x ′ = ax+ b), q 2 ), the set {q 1 }×N is a subset of P re * (↑(q 2 , b)). For any negative transition (q 1 , (x ′ = ax+b), q 2 ), we have (q 1 , 0) → (q 2 , b). If M is a WSTS, by monotony, for any n ≥ 0, there exists a path

(q 1 , n) * -→ (q 2 , b ′ ) ≥ (q 2 , b) because (q 1 , n) ≥ (q 1 , 0). This implies that {q 1 } × N is a subset of P re * (↑(q 2 , b)).
In the other direction, let there be a transition (q 1 , n) → (q 2 , an+b) and (q 1 , n ′ ) ≥ (q 1 , n). If the transition is positive, i.e. a ≥ 0, then we directly have the transition (q 1 , n ′ ) → (q 2 , an ′ +b) ≥ (q 2 , an+b). If the transition is negative, then we have that (q 2 , an+b) ≤ (q 2 , b). Since (q 1 , n ′ ) ∈ P re * (↑(q 2 , b)) (by hypothesis, since it is a negative transition), hence we have that (q 1 , n ′ ) * -→ (q 2 , b ′ ) ≥ (q 2 , b) ≥ (q 2 , an + b). Hence, M is monotone. Therefore, M is a WSTS iff for all negative transitions (q 1 , (x ′ = ax + b), q 2 ), the set {q 1 } × N is a subset of P re * (↑(q 2 , b)). Now, since P re * (↑(q, n)) is computable, we can check that for each negative transition (q 1 , (x ′ = ax + b), q 2 ), the set {q 1 } × N is a subset of P re * (↑(q 2 , n)) to determine whether M is a WSTS or not. ◭ ◮ Example 27. Let us consider machine M 1 in Figure 1 and its negative transition (q 1 , x ′ = 19 -x, q 1 ). We observe that the set P re * (↑(q 1 , 19)) = {q 1 , q 2 } × {n : n ≥ 19} does not contain {q 1 } × N, hence machine M 1 is not a WSTS. However, in this example (Figure 1), if we replace the transition (q 1 , (x ′ = x -13), q 2 ) by (q 1 , (x ′ = x + 1), q 2 ), we will get a new machine M 2 which is still not a 1-VASS, but it is a WSTS.

Let us focus our attention to positive AVASS now. We know that for positive 1-AVASS reachability is decidable from Corollary 24. We show that reachability is undecidable for positive 2-AVASS by reduction from Post's Correspondence Problem (PCP) [START_REF] Halava | Another proof of undecidability for the correspondence decision problem -had I been emil post[END_REF]. Our result completes the view about decidability of reachability for VASS extensions in small dimensions. As a matter of fact, reachability is undecidable for VASS with two resets in dimension 3 (to adapt the proof in [START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF]), hence for positive 3-AVASS but it is decidable for VASS with two resets in dimension 2 [START_REF] Finkel | Reachability for two-counter machines with one test and one reset[END_REF]. If we replace resets by affine functions, reachability becomes undecidable in dimension two.

q 0 q 1 q 2 I, -1 -1 ( I, 0) 0, 1 1
2 |a1| 0 0 2 |b1| , (a 1 ) 2 (b 1 ) 2 2 |a2| 0 0 2 |b2| , (a 2 ) 2 (b 2 ) 2 2 |a3| 0 0 2 |b3| , (a 3 ) 2 (b 3 ) 2 2 |ak| 0 0 2 |bk| , (a k ) 2 (b k ) 2 ...
Reichert gives in [21] a reduction from the Post correspondence problem to reachability in a subclass of 2-AVASS and we may remark that his proof is still valid for positive 2-AVASS. Blondin, Haase and Mazowiecki made some similar observations [START_REF] Blondin | Affine extensions of integer vector addition systems with states[END_REF] for subclasses of 3 -Z-AVASS, with positive matrices. Our proof is essentially the same as [21].

◮ Theorem 28. Reachability is undecidable for positive 2-AVASS.

Proof. Suppose we are given an instance of PCP, i.e. we are given a 1 , ..., a k , b 1 , ..., b k ∈ {0, 1} * for some k ∈ N. We want to check if there exists some sequence of numbers n 1 , ..., n ℓ ∈ {1, ..., k} such that a n1 ...a n ℓ = b n1 ...b n ℓ (concatenated as strings).

We will construct the positive 2-AVASS as demonstrated in Figure 2, where |a i | refers to the length of the string, and (a i ) 2 refers to the number encoded by the string a i if read in binary (most significant digit to the left). The idea is that we use the two counters to store the value of (a n1 ...a n ℓ ) 2 and (b n1 ...b n ℓ ) 2 for any n 1 , ..., n ℓ . But we first increment each counter to keep track of leading zeroes. Now, the configuration (q 2 ; 0, 0) is reachable from (q 0 ; 0, 0) in the positive 2-AVASS described in Figure 2 iff the given PCP has an affirmative answer. Hence, checking reachability in positive d-AVASS is undecidable for d ≥ 2. ◭ Also, we note that positive-AVASS are well-structured with strong monotony. Hence coverability is decidable [START_REF] Finkel | A well-structured framework for analysing Petri net extensions[END_REF]. If we look at totally-positive AVASS, we can see that coverability is already decidable by the same argument. However, reachability is also decidable.

◮ Theorem 29. Reachability is decidable in totally-positive AVASS for any dimension.

Proof. Let M = (Q, →) be a totally-positive d-AVASS. Given (q 0 ; n 1 , ..., n d ), suppose we want to check reachability of (q f ; m 1 , ..., m d ). Let N = max{m 1 , ..., m d }. Let f N : N → {1, ..., N, ω} be the function which is identity on {1, ..., N } and maps {N +1, ...} to ω. Extend this function to the set N d component-wise. Since M is totally-positive, we can restrict our search space from Q × N d to Q × {0, ..., N, ω} d by applying f N to each configuration and using the following arithmetic rules: 0.ω = 0, and for all k ≥ 1, k.ω = ω and ω + k = ω.

We claim that if (q f ; m 1 , ..., m d ) is reachable, then it is reachable in this restricted searchspace. This follows from the fact that given any element (n 1 , ..., n d ) of N d , and a totally positive transition t = (A, b), we will have that t(f N (n 1 , ..., n d )) = f N (t(n 1 , ..., n d )) (t acts on f N (n 1 , ..., n d ) to give an element in {0, ..., N, ω} d ). This is because a totally positive transition cannot decrease a value other than by multiplying it by 0, hence any value greater than N will continue to be greater than N . Also note that, by choice of N , f N (m 1 , ..., m d ) = (m 1 , ..., m d ). Once we have this, we can make an induction on the length of the path to see that if (q f ; m 1 , ..., m d ) is reachable, it is reachable in the restricted search-space Q × {0, ..., N } d .

Since Q × {0, ..., N, ω} d is finite, this shows decidability of reachability. ◭

Conclusion and perspective

We introduced two variants of the well structured problem for PCM and we solve it for many classes of PCMs. Moreover, we answer the decidability questions for reachability and coverability for classes of PCMs and AVASSs (we summarise the results of Section 4 in Figure 3). Many open problems can be attacked like the complexity of reachability for 1-AVASS (reachability is NP for 1-VASS and PSPACE for polynomial VASS), the size of P re * of a 1-AVASS (and its relation with the theory of flattable VASS [18]), and the decidability of the property for a Presburger relation on N d to be a well-quasi ordering for d ≥ 2.

We also open the way to study the decidability of the well structured problems (for various orderings) for many other models like pushdown counter machines, FIFO automata, Petri nets extensions. For instance, we wish to solve the well structured problems for FIFO automata. We know that lossy FIFO automata are well structured (for the subword ordering) but what is the class of perfect FIFO automata which is well structured (for the prefix ordering)? We write φ 0 in disjunctive normal form. Hence, φ 0 will be written as a disjunction of formulae ψ i where each ψ i can be written in the form (φ 1 ∧φ 2 ∧φ 3 ∧φ 4 ∧φ 5 ∧φ 6 ∧φ 7 ∧φ 8 ∧φ 9 ) where: Let ψ be one conjunctive clause in the DNF for φ 0 . Hence

φ 1 is a conjunction of formulae of form ax + by ≤ n with a ≥ 1, b ≥ 1 φ 2 is a conjunction of formulae of form ax + by ≤ n with a ≥ 1, b ≤ 1 φ 3 is a conjunction of formulae of form ax + by ≥ n with a ≥ 1, b ≥ 1 φ 4 is a conjunction of formulae of form ax + by ≥ n with a ≥ 1, b ≤ 1 φ 5 is a conjunction of formulae of form ax ≥ n with a ≥ 1 φ 6 is a conjunction of formulae of form ax ≤ n with a ≥ 1 φ 7 is
ψ 0 = ψ 1 ∧ ψ 2 ∧ ψ 3 ∧ ψ 4 ∧ ψ 5 ∧ ψ 6 ∧ ψ 7 ∧ ψ 8 ∧ ψ 9
where each ψ i conforms to above specifications. We show that we only need to be concerned with ψ 9 . This is because, suppose N = (n 1 , n 2 , n 3 , ...) is a sequence for which we need to produce an ascending pair to check wqo of φ. For each n i , there are only finitely many n j , j > i such that ψ 1 (n i , n j ) is satisfied. In this case, we can remove those finitely many n j . We do this for all n i to get a sequence N ′ = (n ′ 1 , n ′ 2 , n ′ 3 , ...) thus rendering ψ 1 , hence ψ 0 unsatisfiable by x, y ∈ N ′ . Clearly, if N ′ has an ascending pair, so does N . Hence it is sufficient to check existence of ascending pair in N ′ . Hence, if ψ 1 is non-empty, then we can simply disregard ψ 0 since it will never be satisfied in N ′ .

We can make a similar argument for ψ 4 . For ψ 2 and ψ 3 , we make the dual argument, that for all n i , there are only finitely many n j , j > i such that ψ 3 (n i , n j ) ∧ ψ 4 (n i , n j ) is not satisfied. Once we remove all such offending pairs to get N ′ , we will get that every pair in N ′ satisfies φ 3 ∧ φ 4 , hence we can also remove them from consideration.

For ψ 5 and ψ 7 there are only finitely many n i such that ψ 5 (n i , n) or ψ 7 (n, n i ) is satisfiable for any n ∈ N. We can remove these n i to render ψ 5 and ψ 7 redundant. For ψ 6 and ψ 9 we again make the dual argument, removing the finitely many n i which can satisfy ψ 5 and ψ 7 . Hence, we can disregard each ψ i .

So, now, for the given formula φ and a sequence N , we will get a sequence N ′ subsequence of original sequence, and a new formula φ ′ comprising of disjunctions of formulae of form φ 5 , where each formula ψ i consists of conjunctions which look like (a i,j x + b i,j y = ni,j c i,j ). We now let N = lcm ∀i∀j {n i,j }. We can transform φ ′ to comprise entirely of formulae of form a i,j x + b i,j y = N c i,j by multiplying each individual formula and breaking it into disjunctions. Now, let ψ i consist of conjunctions of (a i,j x + b i,j y = ni,j c i,j ). By checking for all x ∈ {1, ..., N }, y ∈ {1, ..., N }, we can reduce this to disjunctions of ψ i of the form (x = N a i ∧ y = N b i ). Now, we look for n 0 ∈ {1, ..., N } such that ¬φ ′ (n 0 , n 0 ). In other words, ∄ disjunction ψ i ≡ (x = N n 0 ∧ y = N n 0 ). This can again be done finitely. Now, the claim is that φ is a wqo iff no n 0 exists. Clearly, if such an element exists, then φ is not a wqo, because we can take an M such that N |M and M is large enough such that we can ignore all subformulae of the form φ 1 , ..., φ 4 , and then (M + n 0 , M + N + n 0 , (M + 2N ) + n 0 , ..., (M + aN ) + n 0 , ...) has no ascending pair.

Similarly, if no such element exists, then given any sequence (n 1 , n 2 , ...), we can remove small enough terms, and then look at each term mod N . Since no such element exists, we will have some repetition in the infinite sequence mod N and that will give us an ascending pair. Thus we have demonstrated a decision procedure for whether a Presburger formula φ encodes a wqo. ◭

M :

q q ′ q ′′ c1=0? c 1 = 0 ? =⇒ N : q q ′ q ′′ c4-- c4=0? c1--, c3--, c4++ c3=0? c1=0? c 1 = 0 ? c1++, c3++, c4-- c1++,

Section 3

Well structured problem for 2-Minsky machines

We shall first show a construction for 4 counter Minsky machines satisfying conditions (1) and [START_REF] Blondin | The complexity of reachability in affine vector addition systems with states[END_REF].

Construction of a 4 counter Minsky machine N 2 :

Let (M, q 1 ) be given. We will use 4 counters to simulate M in such a way that we can get all the desirable properties. We will use a configuration (q; c 1 , c 2 , c 3 , c 4 ) of N 2 to correspond to the configuration (q; c 1 -c 3 , c 2 -c 3 ) of M . The procedure to generate a 4-counter Minsky machine N 2 is as follows: Let M = (Q, → M , q 0 ). We define N 2 = (Q 0 , → N , (q 0 ; 1, 1, 1, 0)) where Q 0 is a superset of Q as will be made clear. To get N 2 , we will make the following modifications to M : Replace zero-tests in M with a circuit which checks if the respective counter equals c 3 . We will use c 4 and add required additional control-states to implement such a test as illustrated in figure 4a. Now, from each control-state q, including the new ones added in previous step, add another circuit as illustrated in figure 4b which allows one to reach (q 0 ; n, n, n, 0) for any n ≥ 1. Note that q 0 is the initial state of M . We shall again call it a "reset-circuit" since (q 0 ; n, n, n, 0) in N 2 corresponds to (q 0 , 0, 0) in M . Hence this transition acts as a Case 1: s < ∞. In this case, since the cycle can only be fired by a finite number of inputs, we can simply take each input n and compute P ost c i (n) for all i till c can no longer be activated, or it repeats. Then, we can decide whether or not n ∈ P re c * (range ∧ mod) based on if any of the reachable values satisfy range ∧ mod. Case 2: s = ∞, a ≤ 1. Note that since the guard is upward closed, it implies that the cycle is positive. Hence the net transition is x ′ = ax + b for a ≥ 0. If a = 0, we are done. If a = 1, then the cycle is a translation. In this case, P re c * (range ∧ mod) is again computable using modulo relations. Case 3: s = ∞, a ≥ 2. Let N = -b a-1 . The first thing to observe is that for all n > N , P ost c (n) > n. Hence, upon repeated application, n keeps increasing. If s 1 < ∞, then n ≥ max{s 1 , N } =⇒ n / ∈ P re c * (range ∧ mod). With only finitely many values left to consider, we can again compute P ost c i (n) for all r ≤ n ≤ max{s 1 , N } to determine whether n ∈ P re c * (range ∧ mod). If s 1 = ∞, then for values n ≥ N , we only need to be concerned with their value mod d. Hence, we can first compute the set of values ℓ 1 , ..., ℓ k mod d such that for some j, we have P ost c j (ℓ i ) = d d 1 . Then we know that (n ≥ N ∧ n = d ℓ i ) =⇒ n ∈ P re c * (range ∧ mod).

For n ≤ N , we can again compute P ost c i (n) to determine whether n ∈ P re c * (range ∧ mod). Since it does not go off to infinity, it will again terminate or repeat. Thus, we have shown that for any cycle c, we can compute P re c * (φ q ). ◭ ◮ Corollary 24. Reachability (hence coverability and control-state reachability) for 1-AVASS is decidable.

Proof. Suppose we want to check reachability of (q 2 , n 2 ) from (q 1 , n 1 ). Once we have computed P re * (q 2 , n 2 ), we can check easily whether (q 1 , n 1 ) ∈ P re * (q 2 , n 2 ) to solve reachability. Once we have reachability, we can show a reduction from coverability to reachability to show that coverability is also decidable for 1-AVASS, as follows. Suppose we want to check coverability of (q 2 , n 2 ). We can add two new control-states q 3 and q 4 and add the transitions (q 2 , (x ′ = x-n 2 ), q 3 ) and (q 3 , (x ′ = 0), q 4 ). Now, (q 4 , 0) is reachable iff (q 2 , n 2 ) coverable. ◭

Figure 1

 1 Figure 1The counter machine M1

Figure 2

 2 Figure 2 Construction for undecidability of reachability for positive 2-AVASS by reduction from PCP.

Figure 3

 3 Figure 3 Showing reachability and coverability results for various AVASS models.

  a conjunction of formulae of form by ≥ n with b ≥ 1 φ 8 is a conjunction of formulae of form by ≤ n with b ≥ 1 φ 9 is a conjunction of formulae of the form ax + by = n p with a, b ≥ 0.

0 c 1 Figure 4

 014 Figure 4 Construction of a 4 counter Minsky machine N2

  2-AVASS since translations are affine functions. A zero test on the first counter can be done by having a transition However, if we consider strong monotony instead of monotony, the above undecidability results can be turned into a decidability result. Strong monotony can be expressed in Presburger arithmetic as follows:

	labelled by	-1 0 0 1	,	0 0	, and similarly for second counter. Since we can implement

both increment/decrements and zero-tests with 2-AVASS, we can simulate 2-counter Minsky machines with 2-AVASS. Note that we can extend this result to d-AVASS simulating dcounter Minsky machines. As a direct consequence of this and Theorem 15, we have that: ◮ Corollary 16. The well structured problem for 2-AVASS is undecidable. φ∈Φ (∀x 1 ...∀x d ∀x ′ 1 ...∀x ′ d ∀y 1 ...∀y d (( d i=1

18

  Jérôme Leroux and Grégoire Sutre. On flatness for 2-dimensional vector addition systems with states. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 -Concurrency Theory, 15th International Conference, London, UK, August 31 -September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004.

	19 Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown
	vector addition systems in one dimension. In Automata, Languages, and Programming -42nd
	International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II,
	pages 324-336, 2015.

Matthias Horbach, Marco Voigt, and Christoph Weidenbach. The universal fragment of presburger arithmetic with unary uninterpreted predicates is undecidable. CoRR, abs/1703.01212, 2017.

Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1967.

Julien Reichert. Reachability games with counters : decidability and algorithms. (Décidabilité et complexité de jeux d'accessibilité sur des systèmes à compteurs). PhD thesis, École normale supérieure de Cachan, France, 2015.

Rüdiger Valk. Self-modifying nets, a natural extension of petri nets. In Giorgio Ausiello and Corrado Böhm, editors, Automata, Languages and Programming, Fifth Colloquium, Udine, Italy, July 17-21, 1978, Proceedings, volume 62 of Lecture Notes in Computer Science, pages 464-476. Springer, 1978.

The work reported was carried out in the framework of ReLaX, UMI2000 (ENS This work was also supported by the grant ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS). Reachability Coverability 1-PCM (functional ) U U [Corollary 19] 1-AVASS D [Corollary 24] D d-totally positive AVASS D [Theorem 29] D d-positive AVASS (d ≥ 2)

Appendix 6.1 Section 2 ◮ Proposition 2. [START_REF] Demri | Model-checking ctl* over flat presburger counter systems[END_REF] The property for a d-dim PCM to be functional, is decidable in NP.

Proof. Let M = (Q, Φ, →) be a given d-dim PCM. Functionality can be expressed in Presburger arithmetic as follows:

Hence, the validity of this formula can be decided, and so, functionality is decidable. ◭ ◮ Proposition 7. The well structured problem for 1-arithmetic counter machines is undecidable.

Proof. Since first order (FO) logic is undecidable, we can have a reduction from decidability of FO to checking whether a given arithmetic counter machine is well-structured. Let φ be a given FO formula with no free variables. Define the 1-arithmetic counter machine M = ({q 0 }, {φ 0 }, →), where φ 0 = ((x 1 = 0 ∧ y 1 = 2) ∨ φ) and →= {(q 0 , φ 0 , q 0 )} and let S M be its associated transition system. Hence, if φ is a tautology, then for all m, n ≥ 0, the transition (q 0 , m) → (q 0 , n) exists in S M . Hence S M is a well-structured transition system. However, if φ is false, then S M is not well-structured since there is a transition (q 0 , 0) → (q 0 , 2), but there is no transition from (q 0 , 1) ≥ (q 0 , 0) which violates monotony. Hence S M is a WSTS iff φ is a tautology. ◭ ◮ Proposition 9. The property for a decidable ordering on N to be a well ordering is undecidable.

Proof. We will have a reduction from Halting Problem to show undecidability of checking whether a relation on N is a wqo. Let M be a Turing machine and ≤ M its associated decidable relation defined as follows. For all i, j: we have i ≤ M i and i ≤ M i + j iff M does not halt in i + j steps and i + j ≤ M i if M halts in at most i + j steps; hence N is totally ordered by the decidable ordering

is not a well ordering because it is not well-founded. Therefore, checking whether an ordering ≤ encodes a well ordering is undecidable.

◭ ◮ Proposition 10. The property for a Presburger relation on N to be a well-quasi ordering is decidable.

Proof. We can check if a Presburger formula encodes a quasi ordering since reflexivity and transitivity are Presburger-expressible. Consider a Presburger formula φ with two free variables x and y, encoding a relation on N. We can assume φ is a quasi ordering. We want to determine if it is a wqo. We can do quantifier elimination to arrive at φ 0 , a quantifier-free formula over the predicates {+, ≤, <, =, >, ≥, = n } where a = n b iff a = b mod n.

counter-reset. Note that adding such a transition to M will not affect its reachability set. The "reset-circuit" will be used to ensure condition [START_REF] Blondin | Affine extensions of integer vector addition systems with states[END_REF]. Finally, add a transition (q 0 ; 0, 0, 0, 0) → N (q 1 ; 0, 0, 0, 0). This is to ensure property [START_REF] Blondin | The complexity of reachability in affine vector addition systems with states[END_REF]. Note that we can never reach (q 0 ; 0, 0, 0, 0) from the initial configuration (q 0 ; 1, 1, 1, 0) in any run of N 2 since the "reset-circuit" resets to (q 0 ; n, n, n, 0) for n ≥ 1. Hence adding this transition does not affect the reachability set of N 2 . Now, we will show that the above construction indeed satisfies conditions (1) and [START_REF] Blondin | The complexity of reachability in affine vector addition systems with states[END_REF].

◮ Lemma 30. The 4 counter Minsky machine N 2 satisfies condition [START_REF] Blondin | Affine extensions of integer vector addition systems with states[END_REF].

Proof. Suppose all control-states are reachable in M . Let there be a transition (q; n 1 , n 2 , n 3 , n 4 ) → N (q ′ ; m 1 , m 2 , m 3 , m 4 ) and a configuration (q

). Since all control-states in M are reachable, there exists a path (q 0 ; 0, 0) * -→ M (q ′ ; n 1 , n 2 ). Choose N ≥ max{m 1 , m 2 , m 3 , m 4 }, and take the "reset-circuit" (q Proof. Since N 2 is a WSTS, (q 0 ; 0, 0, 0, 0) → N (q 1 ; 0, 0, 0, 0) =⇒ (q 0 ; 1, 1, 1, 0)

The well structured problem for 2-dim Minsky machines is undecidable.

Proof. Since we have given the appropriate construction, by Lemma 11, we have that checking whether 4-counter Minsky machines are WSTS is undecidable. We will use the fact that a d-dim Minsky machine can be simulated by a 2-counter Minsky machine [20]. Let N 2 be the corresponding 4-counter Minsky machine for (M, q 1 ) which satisfies conditions (1) and [START_REF] Blondin | The complexity of reachability in affine vector addition systems with states[END_REF]. Let N ′ 2 be the 2-counter Minsky machine which simulates N 2 . Let N ′′ 2 be the 2-counter machine obtained by adding another "reset" circuit to N ′ 2 which allows reachability to (q 0 ; 0, 0) from any configuration. Then, N ′′ 2 will satisfy conditions (1) and (2) because N ′′ 2 is simulating N 2 which satisfies conditions (1), (2) and we are allowing reset to initial configuration in N ′′ 2 . Hence, by Lemma 11 again we have that the well structured problem for 2-dim Minsky machines is undecidable. ◭

Section 4

◮ Lemma 20. For any transition t, and any simple cycle c, given φ q , P re t (φ q ) and P re c * (φ q ) are both Presburger expressible and effectively computable.

Proof. Let φ ≡ ∨ k i=1 (range i ∧ mod i ). First we note that P re c * (φ q ) = ∪ k i=1 P re c * (range i ∧ mod i ), so we will focus on a single range ∧ mod clause in φ.

For a transition t, we can compute P re t by looking at each range ∧ mod clause in φ q , and computing its inverse.

Similarly, we can compute P re c i for any i ∈ N. We will show that P re c * (range ∧ mod) is also computable.

Given a cycle c rooted at q, with guard r ≤ n ≤ s (s possibly ∞) and the meta-transition y = ax + b, let range ≡ (r 1 ≤ n ≤ s 1 ) and mod ≡ (n = d d 1 ). By P ost c i (n) we denote i successive applications of a cycle to n. To show that P re c * (φ q ) is effectively computable, we will look at multiple cases: