Antoine Clarinval
email: antoine.clarinval@unamur.be

Benoît Duhoux
email: benoit.duhoux@uclouvain.be

Bruno Dumas
email: bruno.dumas@unamur.be

Supporting Citizen Participation with Adaptive Public Displays: A Process Model Proposal Proposition d'un modèle de processus pour les aichages publics adaptatifs supportant la participation citoyenne

Keywords: Citizen participation, adaptive public display, process model Participation citoyenne, aichage public adaptatif, modèle de processus

In recent years, public displays have been studied as a way to foster citizen participation. However, their surroundings and users are prone to high variability, which makes it tedious to accommodate dierent contexts with an optimal participation experience. In this paper, we propose adaptive public displays as a lead for solution in tackling this issue. From a review of the motivators and barriers aecting citizen's interaction with public displays we defined a process model destined to serve as a guide for designers of such systems.

INTRODUCTION

With the emergence of the smart city paradigm, many cities have developed technological solutions in an aempt to answer the challenges they face (e.g. road congestion, waste management). However, research showed that these initiatives are doomed to failure when cities do not give enough consideration to the specific needs of their territory and inhabitants [START_REF] Paola | Comparing smart and digital city: initiatives and strategies in Amsterdam and Genoa. Are they digital and/or smart?[END_REF][START_REF] Robert | Will the real smart city please stand up? Intelligent, progressive or entrepreneurial[END_REF]. As a result, initiatives aiming at engaging citizens in the public life have emerged and methods to achieve this have been extensively proposed [START_REF] Simonofski | Co-creating e-Government Services: An Empirical Analysis of Participation Methods in Belgium[END_REF]. Methods such as workshops [START_REF] Noyman | Finding Places: HCI Platform for Public Participation in Refugees' Accommodation Process[END_REF] and citizen participation platforms [START_REF] Sousa | Liberopinion: A web platform for enhancing e-democracy[END_REF] have proved valuable, but show a representativity limit as they tend to aract "usual suspects" with a prior interest in civic engagement.

Public displays have been researched as a citizen participation means [START_REF] Hespanhol | Vote as you go: blending interfaces for community engagement into the urban space[END_REF][START_REF] Hosio | Exploring civic engagement on public displays[END_REF] and have been successful in enticing much more participation than traditional methods [START_REF] Goncalves | Citizen motivation on the go: The role of psychological empowerment[END_REF] due to their innovative, contextualized (i.e. the content shown on the display is related to its location), collaborative and opportunistic (i.e. citizens encounter public displays without planning to do so) nature. Public displays are oen in the form of a voting systems inviting passersby to answer displayed questions, either via a multiple-choice answer (e.g. [START_REF] Claes | The Bicycle Barometer: Design and Evaluation of Cyclist-Specific Interaction for a Public Display[END_REF][START_REF] Hespanhol | Vote as you go: blending interfaces for community engagement into the urban space[END_REF][START_REF] Taylor | Viewpoint: empowering communities with situated voting devices[END_REF]) or free-text allowing richer feedback (e.g. [START_REF] Hosio | Exploring civic engagement on public displays[END_REF][START_REF] Schroeter | Engaging new digital locals with interactive urban screens to collaboratively improve the city[END_REF]). Various techniques allow users to vote with a public display [START_REF] Ardito | Interaction with large displays: A survey[END_REF], including direct touch [START_REF] Hosio | Exploring civic engagement on public displays[END_REF], body movements [START_REF] Valkanova | MyPosition: sparking civic discourse by a public interactive poll visualization[END_REF], and the use of external devices such as smartphones [START_REF] Schroeter | Engaging new digital locals with interactive urban screens to collaboratively improve the city[END_REF] and pressure plates [START_REF] Steinberger | Vote with your feet: Local community polling on urban screens[END_REF]. Recent work is also studying the potential of immersive public displays [START_REF] Du | Interactive immersive public displays as facilitators for deeper participation in urban planning[END_REF].

Deploying interfaces in the urban environment for any citizen to use raises challenges, as the surroundings and the characteristics of the users change constantly. Consequently, a public display IHM'19 Adjunct, December 10-13, 2019, Grenoble, France Supporting Citizen Participation with Adaptive Public Displays: a Process Model Proposal 10:2 cannot provide an optimal interaction at all time, which in turn hinders its citizen participation purpose. The challenge of the adaptation of public displays to such a changing environment has been underlined in the literature [START_REF] Ananny | Handbook of research on urban informatics: The practice and promise of the real-time city[END_REF][START_REF] Koch | Information radiators: using large screens and small devices to support awareness in urban space[END_REF], and some previous work has focused on the adaptation of public displays according to one or several context factors. A well-know example is proxemic interaction [START_REF] Ballendat | Proxemic interaction: designing for a proximity and orientation-aware environment[END_REF][START_REF] Greenberg | Proxemic interactions: the new ubicomp?[END_REF] that adapts the content shown and the features according to the distance between the user and the display. Previous implementations of proxemic interaction have proposed to adapt the content and content presentation to the position of the user [START_REF] Cheung | Proxemics-based visual concepts to aract and engage public display users: Adaptive content motion and adaptive user shadow[END_REF][START_REF] Kim | Finding Satisfactory Transparency: An Empirical Study on Public Transparent Displays in a Shop Context[END_REF]. Other works have focused on the user aention and interest, which includes his proximity and orientation relatively to the display [START_REF] Wang | Proxemic peddler: a public advertising display that captures and preserves the aention of a passerby[END_REF] and the presence of other users [START_REF] Schiavo | Sensing and reacting to users' interest: an adaptive public display[END_REF]. A public display adapting to the height of the user by allowing the user to move interface elements was presented in [START_REF] Parker | Towards Adaptive Height-Aware Public Interactive Displays[END_REF]. Kurdyukova [START_REF] Kurdyukova | Adaptation on personalized public displays driven by social context[END_REF] has studied how public displays can be adapted according to the user (e.g. user interest, aention, emotional state) and social environment factors (e.g. number of people around the display, their age and gender). However, none of the public displays described in these works serve a citizen participation purpose, and they tackle adaptation to one changing element of context for the most part. In this paper, we address this gap by exploring how adaptive public displays can be modelled from a designer's point of view. From an extensive literature review, we identified the motivators and barriers impacting interaction with public displays supporting citizen participation. These served as a basis to the process model we defined to guide designers of adaptive public displays. An hypothetical adaptive voting system running on a public display is described as illustrative example of the process model usage.

RUNNING EXAMPLE: A VOTING SYSTEM

Before describing the process model and the methodology that guided us in its development, we first present a running example of adaptive public display in order to illustrate how adaptation can yield added value. This example is an adaptive voting system that gathers the opinion of citizens on a given issue, by prompting them to answer a question shown on a public display.

Venue

Motiv. Barriers Both

PerDis 0 0 2 C&T 0 0 2 CHI 1 0 2 DIS 0 1 1 CSCW 0 0 2 Other ACM 1 1 3 Other 0 1 3 Total 2 3 15

Table 1: Number of articles reporting motivators and barriers to interaction

Fig. 1 depicts a feature model to design this adaptive system. Citizens passing by the display are informed about the issue with contextual information by text, pictures or videos. They can also give their opinion on the question. Depending on the surrounding environment (e.g. the weather or their time availability), they can provide an answer with predefined choices or in a richer way such as a plain text opinion. In addition, the vote can be performed through various interaction modalities [START_REF] Ardito | Interaction with large displays: A survey[END_REF] such as direct touch on the display (e.g. [START_REF] Hosio | Exploring civic engagement on public displays[END_REF]), body movements (e.g. [START_REF] Valkanova | MyPosition: sparking civic discourse by a public interactive poll visualization[END_REF]), and using an external device (e.g. [START_REF] Schroeter | Engaging new digital locals with interactive urban screens to collaboratively improve the city[END_REF]). Finally, the citizen can see the current results for the question.

A feature model is a good way to represent the commonalities and the variabilities of an adaptive system [START_REF] Kyo | Feature-Oriented Domain Analysis[END_REF], which is why we chose to model the voting system using this representation. The nodes represent the functionalities of the system while the edges describe the hierarchical relations between IHM'19 Adjunct, December 10-13, 2019, Grenoble, France Supporting Citizen Participation with Adaptive Public Displays: a Process Model Proposal 10:3 the features. A Mandatory relation implies that the child feature is always present in the system. An Or relation forces that at least one of the child features is present in the system at runtime.

PROCESS MODEL FOR ADAPTIVE PUBLIC DISPLAYS

Even if many motivators encourage citizens to interact with public displays for participation, many barriers dissuade them to use such systems. We believe that adaptive public displays could increase the interactions in such citizen engagement by strengthening these motivators and lowering these barriers. For that we created a process model to help the designers to conceive adaptive public displays.

In this section, we first describe the methodology used to define this process model and then we present the process model.

Methodology

Previous empirical contributions presenting public displays supporting citizen participation have reported on the motivators (resp. barriers) encouraging (resp. deterring) users to interact with their systems. These serve as foundation for the process model we propose. Its goal is to improve the citizen participation experience by leveraging adaptation to strengthen motivators and lower barriers.

In order to extract an exhaustive list of these motivators and barriers, relevant literature (i.e. empirical works proposing public displays for citizen participation) was collected following a systematic approach. A keyword search was defined following [START_REF] Peicrew | Systematic reviews in the social sciences: A practical guide[END_REF] and was composed of terms related to public displays and citizen participation. The former keywords were refined throughout the review to include synonyms and cover related fields, whereas the laer were reused from a previous systematic literature review on citizen participation [START_REF] Simonofski | Reexamining Eparticipation: Systematic Literature Review on Citizen Participation in E-government Service Delivery[END_REF]. The search was performed on the title and keywords fields of the articles on the ACM Digital Library, IEEEXplore, and ScienceDirect. Bibliographies of the selected articles were perused as well to extend coverage. In total, 34 articles were captured, 27 of which report on motivators and/or barriers to interaction. We only noted the factors that are reported sometimes as a motivator and sometimes as a barrier in the literature. Factors impacting interaction solely as motivator (e.g. honeypot eect, playfulness) or as barrier (e.g. display blindness, interaction blindness) were set aside for these papers, as they inform general design recommendations rather than opportunities for adaptation. 20 articles report on motivators and barriers relevant for adaptation. Table 1 details the number of articles reporting on motivators and barriers, for each publisher. Table 2 lists the factors impacting interaction along with the articles reporting them as motivator, barrier, or both. When, hoW and What). Starting from an interest of adaptation in the intention to increase the motivators and/or decrease the barriers, the designers must design the source, the time, the approach based on the time and the target of the adaptation. Furthermore, with this process model, the designers can assess the impact of the adaptation in a field seing by measuring the dierence between the eective and the intended eect on motivators/barriers to confirm or not the interest of adaptation. Each of these steps are described and exemplified below and illustrated in Fig. 3. Interest of adaptation. Designers must first think about why an adaptation can strengthen the motivators or lower the barriers to citizen participation. In our voting case study, the main objective is to increase the participation of the voters. So for that, the designers must also consider a way to gather feedback from citizens having less time available or increase their topic interests.

Process model

Source Target

Time

Interest of adaptation

Increase the participants

Source. Aer considering why an adaptation is interesting, they must define who causes the adaptation. In adaptive systems, the perception of the environment leads to an adaptation to refine the behavior of the system [START_REF] Bey | Raaela IHM'19 Adjunct[END_REF]. For example, in context-aware systems 1 , this environment can be defined 1 a specific field of adaptive systems by the users (e.g. the time they have), by external information (e.g. the weather) and by physical information (e.g. the size of the screen) [START_REF] Coutaz | Context is Key[END_REF][START_REF] Mens | A Context-Oriented Soware Architecture[END_REF]. Based on this definition of the environment, the feedback from the citizen in our voting system can be dierent according to his time or the weather.

Target. They also have to define what/which features (i.e. functionalities) can be adapted according to the environment in which the system runs. For instance, the feature proposing to send a feedback can be adapted according to the surrounding environment. If the citizen has lile time available or if it is raining, giving feedback could consist in choosing from a range of predefined answers. Otherwise, a richer plain-text feedback could be sent. The modality to send a feedback can also vary. Depending on the citizen's preferences, he could send his feedback from an external device preserving privacy or by touching the screen to answer the question in a less private way.

Time. The designers must consider when the adaptation must occur. The adaptation can either be static or dynamic. While a static adaptation is planned entirely by the developer, a dynamic adaptation is planned at runtime for which some behaviors can be refined depending on the surrounding environment in which they run (i.e. the source in our process model) [START_REF] Mckinley | Composing adaptive soware[END_REF]. Even though we mention static time, we only focus on dynamic time in this paper as our scope is adaptive public displays.

Approach. Finally, the designers must also define how the adaptation will occur, in terms of technology. Static approaches as well as an extensive coverage of the existing approaches are out of the scope of this paper. Some dynamic adaptation approaches are briefly discussed. A first approach is based on model-driven engineering approaches even if their solutions are mainly devoted to the user interface adaptation, by relying either on the Cameleon Reference Framework [START_REF] Calvary | A Unifying Reference Framework for multi-target user interfaces[END_REF] such as for example UsiXML [START_REF] Entin Limbourg | Usixml: A user interface description language for context-sensitive user interfaces[END_REF][START_REF] Tesoriero | Extending UsiXML to Support User-Aware Interfaces[END_REF], or on their own architecture such as the three-layered CAUCE architecture [START_REF] Tesoriero | CAUCE: Model-driven Development of Context-aware Applications for Ubiquitous Computing Environments[END_REF], or COMET(s), a soware architectural style and interactors toolkit for plastic user interfaces [START_REF] Demeure | COMET(s), A Soware Architecture Style and an Interactors Toolkit for Plastic User Interfaces[END_REF]. Other approaches dealing with the soware engineering aspects of dynamic adaptation exist, e.g. context-oriented programming [START_REF] Aotani | Featherweight EventCJ: A Core Calculus for a Contextoriented Language with Event-based Per-instance Layer Transition[END_REF][START_REF] Duhoux | Implementation of a Feature-Based Context-Oriented Programming Language[END_REF][START_REF] Ghezzi | Programming Language Support to Context-aware Adaptation: A Case-study with Erlang[END_REF][START_REF] González | Subjective-C: Bringing Context to Mobile Platform Programming[END_REF][START_REF] González | Context Traits: Dynamic Behaviour Adaptation Through Run-time Trait Recomposition[END_REF][START_REF] Hirschfeld | Generative and Transformational Techniques in Soware Engineering II[END_REF][START_REF] Salvaneschi | Context-oriented programming: A soware engineering perspective[END_REF].

CHALLENGES TO ADAPTIVE PUBLIC DISPLAYS

Although this paper has discussed the potential of adaptive public displays supporting citizen participation, the development of such interfaces is fraught with challenges that would be fair to acknowledge.

First, building an adaptive public display is clearly a more complex task for developers than developing a traditional one. However, the soware engineering literature has proposed programming approaches as discussed previously and development tools (e.g. [START_REF] Duhoux | Feature Visualiser: An Inspection Tool for Context-Oriented Programmers[END_REF]) to support developers in this regard. The development of adaptive public displays also requires sensors, which induce additional hardware equipment expenses, thus increasing the already high cost [START_REF] Hosio | What's in it for me: Exploring the real-world value proposition of pervasive displays[END_REF] of public displays. In the context of citizen participation, such displays are oen deployed by local governments, who might be reluctant to deploy costly systems.

Second, one issue that is likely to emerge at some point in the deployment of an adaptive public displays is conflicting contexts. For instance, if the display adapts the content presentation to the age of its user, a conflict can emerge when several users of dierent ages are using the display simultaneously. Previous works have proposed techniques for handling conflicting contexts and are surveyed in [START_REF] Mens | Managing the Context Interaction Problem: A Classification and Design Space of Conflict Resolution Techniques in Dynamically Adaptive Soware Systems[END_REF].

Third, [START_REF] Kurdyukova | Designing trustworthy adaptation on public displays[END_REF] reported that adaptive public displays are likely to lose users' trust if they lack transparency and controllability in their behavior. This issue is critical in the context of citizen participation. Indeed, several studies surveyed in [START_REF] Alzahrani | Analysing the critical factors influencing trust in e-government adoption from citizens' perspective: A systematic review and a conceptual framework[END_REF] noted that the trust in the technology has an important impact on citizen's trust in electronic government (e-government) and on the intention to use e-government systems. Also, [START_REF] Tolbert | The eects of e-government on trust and confidence in government[END_REF] has shown that "increased government trust is produced by improved interactions through e-government." Therefore, mistrust in the adaptive public display would have a heavily detrimental impact on not only the public display use, but also on the eorts toward e-government in general. This calls for careful consideration of user evaluations in adaptive public displays research in order to ensure that they are trusted and accepted by the public.

Fourth, previous literature has highlighted the challenges pertaining to the evaluation of public displays [START_REF] Alt | How to evaluate public displays[END_REF][START_REF] Hornecker | What do lab-based user studies tell us about in-the-wild behavior?: insights from a study of museum interactives[END_REF]. Indeed, whereas laboratory studies are able to predict usability issues, factors related to the environment require a more costly field evaluation to be studied [START_REF] Hornecker | What do lab-based user studies tell us about in-the-wild behavior?: insights from a study of museum interactives[END_REF]. In the case of adaptive public displays, dynamic events have to occur in order for the behavior of the display to be evaluated. Nonetheless, a promising avenue in this regard is controlled in-the-wild evaluation [START_REF] Claes | Controlling in-the-wild evaluation studies of public displays[END_REF] which allows simulating such events in a field seing, thus preserving ecological validity.

CONCLUSION AND FUTURE WORK

Public displays are being deployed in the urban environment as enablers of citizen participation. However, such systems are confronted to a high variability in their environment, making it challenging to provide the most suitable participation experience at all times. In this paper, we studied adaptive public displays as a solution to this issue. We make the following two contributions. First, a literature review of the motivators and barriers impacting interaction with public displays. Second, a process model destined to guide the designers of adaptive public displays based upon it.

As next step, a validation of our proposal is necessary. First, to assess whether adaptive public displays do enhance citizen participation in comparison to traditional ones. Second, to evaluate the eiciency of the process model as a guide for designers.

Figure 1 :

 1 Figure 1: Simplified feature model representing the dierent functionalities of the voting system.

Fig. 2

 2 Fig.2depicts the process model defined to help designers in the creation of adaptive public displays. This model is composed of five steps, each dedicated to one of the five big W questions (Why, Who,

Figure 2 :

 2 Figure 2: The process model destined to help the designers in the creation of adaptive public displays.

Figure 3 :

 3 Figure 3: An instance of the process model where the adaptation proposes dierent ways to answer a survey depending on the time availability of the users to increase the number of participants.

IHM' 19

 19 Adjunct, December 10-13, 2019, Grenoble, France Supporting Citizen Participation with Adaptive Public Displays: a Process Model Proposal 10:5 Supporting Citizen Participation with Adaptive Public Displays: A Process Model Proposal IHM '19 Adjunct, December 10-13, 2019, Grenoble, France

IHM' 19

 19 Adjunct, December 10-13, 2019, Grenoble, France Supporting Citizen Participation with Adaptive Public Displays: a Process Model Proposal 10:6

Table 2 :

 2 Articles reporting factors impacting interaction, as motivator, barrier, or both

	Factor	Motiv. Barrier	Both
	Technology	[29, 52] [39, 58] [22, 23]	[33, 34] [65]	[53]
	Social exposure	[53, 58]	[6, 12] [33] [29, 63]	-
	Time available	[6, 58] [54]	[15, 53]	-
	Topic interest	[39, 54]	[53]	[52, 58] [13]
	Content from others	[53, 63] [34]	[54]	-
	Feedback form	[33]	[53]	-
	Content presentation	[39, 59]	-	[11, 43]
	Perceived impact	[15]	[47, 52]	[59]

ACKNOWLEDGMENTS

The authors would like to thank the European Regional Development Fund (ERDF) for financially supporting this research through the Wal-e-Cities project.


Radu Iosif
email: radu.iosif@univ-grenoble-alpes.fr

Xiao Xu
email: xiao.xu@univ-grenoble-alpes.fr

Alternating Automata Modulo First Order Theories

We introduce first-order alternating automata, a generalization of boolean alternating automata, in which transition rules are described by multisorted firstorder formulae, with states and internal variables given by uninterpreted predicate terms. The model is closed under union, intersection and complement, and its emptiness problem is undecidable, even for the simplest data theory of equality. To cope with the undecidability problem, we develop an abstraction refinement semi-algorithm based on lazy annotation of the symbolic execution paths with interpolants, obtained by applying (i) quantifier elimination with witness term generation and (ii) Lyndon interpolation in the quantifier-free theory of the data domain, with uninterpreted predicate symbols. This provides a method for checking inclusion of timed and finite-memory register automata, and emptiness of quantified predicate automata, previously used in the verification of parameterized concurrent programs, composed of replicated threads, with shared memory.

Introduction

Many results in automata theory rely on the finite alphabet hypothesis, which guarantees, in some cases, the existence of determinization, complementation and inclusion checking methods. However, this hypothesis prevents the use of automata as models of real-time systems or even simple programs, whose input and output are data values ranging over very large domains, typically viewed as infinite mathematical abstractions.

Traditional attempts to generalize classical Rabin-Scott automata to infinite alphabets, such as timed automata [START_REF] Alur | A theory of timed automata[END_REF] and finite-memory automata [START_REF] Kaminski | Finite-memory automata[END_REF] face the complement closure problem: there exist automata for which the complement language cannot be recognized by an automaton in the same class. This makes it impossible to encode a language inclusion problem L(A) ⊆ L(B) as the emptiness of an automaton recognizing the language L(A) ∩ L c (B), where L c (B) denotes the complement of L(B).

Even for finite alphabets, complementation of finite-state automata faces inherent exponential blowup, due to nondeterminism. However, if we allow universal nondeterminism, in addition to the classical existential nondeterminism, complementation is possible is linear time. Having both existential and universal nondeterminism defines the alternating automata model [START_REF] Chandra | Alternation[END_REF]. A finite-alphabet alternating automaton is described by a set of transition rules q a -→ φ, where q is a state, a is an input symbol and φ is a boolean formula, whose propositional variables denote successor states. Our Contribution We extend alternating automata to infinite data alphabets, by defining a model of computation in which all boolean operations, including complementation, can be done in linear time. The control states are given by k-ary predicate symbols q(y 1 , . . . , y k ), the input consists of an event a from a finite alphabet and a tuple of data variables x 1 , . . . , x n , ranging over an infinite domain, and transitions are of the form q(y 1 , . . . , y k ) a(x 1 ,...,xn) -------→ φ(x 1 , . . . , x n , y 1 , . . . , y k ), where φ is a formula in the first-order theory of the data domain. In this model, the arguments of a predicate atom q(y 1 , . . . , y k ) represent the values of the internal variables associated with the state. Together with the input values x 1 , . . . , x n , these values define the next configurations, but remain invisible in the input sequence.

The tight coupling of internal values and control states, by means of uninterpreted predicate symbols, allows for linear-time complementation just as in the case of classical propositional alternating automata. Complementation is, moreover, possible when the transition formulae contain first-order quantifiers, generating infinitely-branching execution trees. The price to be paid for this expressivity is that emptiness of first-order alternating automata is undecidable, even for the simplest data theory of equality [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF].

The main contribution of this paper is an effective emptiness checking semi-algorithm for first-order alternating automata, in the spirit of the IMPACT lazy annotation procedure, originally developed for checking safety of nondeterministic integer programs [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF][START_REF] Mcmillan | Lazy annotation revisited[END_REF]. In a nutshell, a lazy annotation procedure unfolds an automaton A trying to find an execution that recognizes a word from L(A). If a path that reaches a final state does not correspond to a concrete run of the automaton, the positions on the path are labeled with interpolants from the proof of infeasibility, thus marking this path and all continuations as infeasible for future searches. Termination of lazy annotation procedures is not guaranteed, but having a suitable coverage relation between the nodes of the search tree may ensure convergence of many real-life examples. However, applying lazy annotation to first-order alternating automata faces two nontrivial problems:

1. Quantified transition rules make it hard, if not impossible, in general, to decide if a path is infeasible. This is mainly because adding uninterpreted predicate symbols to decidable first-order theories, such as Presburger arithmetic, results in undecidability [START_REF] Halpern | Presburger arithmetic with unary predicates is π 1 1 complete[END_REF]. To deal with this problem, we assume that the first-order data theory, without uninterpreted predicate symbols, has a quantifier elimination procedure, that instantiates quantifers with effectively computable witness terms. 2. The interpolants that prove the infeasibility of a path are not local, as they may refer to input values encountered in the past. However, the future executions are oblivious to when these values have been seen in the past and depend only on the relation between the past and current values. We use this fact to define a labeling of nodes, visited by the lazy annotation procedure, with conjunctions of existentially quantified interpolants combining predicate atoms with data constraints. We use first-order alternating automata to develop practical semi-algorithms for a number of known undecidable problems, such as: inclusion of regular timed languages [START_REF] Alur | A theory of timed automata[END_REF], inclusion of quasi-regular languages recognized by finite-memory automata [START_REF] Kaminski | Finite-memory automata[END_REF] and emptiness of predicate automata, a subclass of first-order alternating automata used to verify parameterized concurrent programs [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF]. Related Work Recognizers for languages over infinite alphabets have found various applications, ranging from Unicode text recognition [START_REF] D'antoni | A symbolic decision procedure for symbolic alternating finite automata[END_REF] to runtime program monitoring [START_REF] Barringer | Rule systems for run-time monitoring: From eagle to ruler[END_REF]. Extending finite automata to infinite alphabets has been considered in the context of symbolic alternating finite automata (s-AFA), whose transitions are labeled with guards taken from a decidable theory of the data domain [START_REF] D'antoni | A symbolic decision procedure for symbolic alternating finite automata[END_REF]. As in our model, s-AFA are closed under union, intersection and complement and emptiness is decidable, due to the lack of registers. However, s-AFA are strictly less expressive than our model, because comparing data at different positions in the input word is not possible.

Constrained Horn clauses (CHC) are a branching computation model widespread in program verification [START_REF] Grebenshchikov | Synthesizing software verifiers from proof rules[END_REF]. The main difference between alternating and bottom-up branching computations is that, in an alternating model, all branches of the computation must synchronize on the same input word. With this in mind, it is possible to express emptiness of first-order alternating automata as the existence of solutions of a CHC over a higher-order theory of data, extended with algebraic data types (lists). The effectiveness of such an encoding depends on the effectiveness of interpolation and witness term generation for theories of algebraic data types [START_REF] Hojjat | Deciding and interpolating algebraic data types by reduction[END_REF].

The alternating automata model presented in this paper extends the alternating automata with variables ranging over infinite data considered in [START_REF] Iosif | Abstraction refinement for emptiness checking of alternating data automata[END_REF]. There all variables were required to be observable in the input. We overcome this restriction by allowing internal (invisible) variables. Another closely related work [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] considers an inclusion between an asynchronous product of automata A 1 × . . . × A n , extended with data variables, and a monitor automaton B. The semi-algorithm defined there was based on the assumption that all variables of the observer B must be declared in the automata A 1 , . . . , A n under check. This limitation can now be bypassed, since the inclusion problem can be encoded as emptiness of a first-order alternating automaton and, moreover, the emptiness checking semi-algorithm can handle invisible variables.

The work probably closest to ours concerns the model of predicate automata (PA) [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF][START_REF] Kincaid | Parallel Proofs for Parallel Programs[END_REF], used in the verification of parameterized concurrent programs with shared memory. In this model, the alphabet consists of pairs of program statements and thread identifiers and is considered infinite because the number of threads is unbounded. Since thread identifiers can only be compared for equality, the data theory in PA is the theory of equality. Even with this simplification, the emptiness problem is undecidable when either the predicates have arity greater than one [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF] or use quantified transition rules [START_REF] Kincaid | Parallel Proofs for Parallel Programs[END_REF]. Checking emptiness of quantifier-free PA is possible semi-algorithmically, by explicitly enumerating reachable configurations and checking coverage by looking for permutations of argument values. However, no semi-algorithm has been given for quantified PA. Dealing with quantified transition rules is one of our contributions.

Preliminaries

For two integers 0 ≤ i ≤ j, we define [i, j] def = {i, . . . , j} and [i] def = [0, i].
We consider two disjoint sorts D and B, where D is an infinite domain and B = { , ⊥} is the set of boolean values true ( ) and false (⊥), respectively. The D sort is equipped with countably many function symbols f : D #( f ) → D ∪ B, where #( f ) ≥ 0 denotes the number of arguments (arity) of f . A predicate is a function symbol p : D #(p) → B that is, a #(p)-ary relation.

We consider the interpretation of all function symbols f : D #( f ) → D to be fixed by the interpretation of the D sort, for instance if D is the set of integers Z, these are zero, the successor function and the arithmetic operations of addition and multiplication. We extend this convention to several predicates over D, such as the inequality relation over Z, and write Pred for the set of remaining uninterpreted predicates.

Let Var = {x, y, z, . . .} be a countably infinite set of variables, ranging over D. Terms are either constants of sort D, variables or function applications f (t 1 , . . . , t #( f ) ), where t 1 , . . . , t #( f ) are terms. The set of first-order formulae is defined by the syntax below:

φ := t = s | p(t 1 , . . . , t #(p) ) | ¬φ 1 | φ 1 ∧ φ 2 | ∃x
. φ 1 where t, s, t 1 , . . . , t #(p) denote terms and p is a predicate symbol. We write φ 1 ∨ φ 2 , φ 1 → φ 2 and ∀x . φ 1 for ¬(¬φ 1 ∧ ¬φ 2 ), ¬φ 1 ∨ φ 2 and ¬∃x . ¬φ 1 , respectively. FV(φ) is the set of free variables in φ and the size |φ| of a formula φ is the number of symbols needed to write it down. A sentence is a formula φ with no free variables. A formula is positive if each uninterpreted predicate symbol occurs under an even number of negations and we denote by Form + (Q, X) the set of positive formulae with predicates from the set Q ⊆ Pred and free variables from the set X ⊆ Var. A formula is in prenex form if it is of the form ϕ = Q 1 x 1 . . . Q n x n . φ, where φ has no quantifiers. In this case we call φ the matrix of ϕ. Every first-order formula can be written in prenex form, by renaming each quantified variable to a unique name and moving the quantifiers upfront.

An interpretation I maps each predicate symbol p into a set p I ⊆ D #(p) , if #(p) > 0, or into an element of B if #(p) = 0. A valuation ν maps each variable x into an element of D. Given a term t, we denote by t ν the value obtained by replacing each variable x by the value ν(x) and evaluating each function application. For a formula φ, we define the forcing relation I, ν | = φ recursively on the structure of φ, as usual. For a formula φ and a valuation ν, we define

[[φ]] ν def = {I | I, ν | = φ} and drop the ν subscript for sentences. A sentence φ is satisfiable if [[φ]] ∅. An element of [[φ]] is called a model of φ. A formula φ is valid if I, ν | = φ
for every interpretation I and every valuation ν. We say that φ entails ψ,

written φ | = ψ if and only if [[φ]] ⊆ [[ψ]].
Interpretations are partially ordered by the pointwise subset order, defined as I 1 ⊆ I 2 if and only if p I 1 ⊆ p I 2 for each predicate symbol p ∈ Pred. Given a formula φ and a valuation ν, we define [[φ]]

First Order Alternating Automata

Let Σ be a finite alphabet Σ of input events. Given a finite set of variables X ⊆ Var, we denote by X → D the set of valuations of the variables X and Σ[X] = Σ × (X → D) be the possibly infinite set of data symbols (a, ν), where a is an input symbol and ν is a valuation. A data word (simply called word in the following) is a finite sequence w = (a 1 , ν 1 )(a 2 , ν 2 ) . . . (a n , ν n ) of data symbols. Given a word w, we denote by w Σ def = a 1 . . . a n its sequence of input events and by w D the valuation associating each time-stamped variable x (i) , where x ∈ Var, the value ν i (x), for all i ∈ [1, n]. We denote by ε the empty sequence, by Σ * the set of finite input sequences and by Σ[X] * the set of finite data words over the variables X.

A first-order alternating automaton is a tuple A = Σ, X, Q, ι, F, ∆ , where Σ is a finite set of input events, X is a finite set of input variables, Q is a finite set of predicates denoting control states, ι ∈ Form + (Q, ∅) is a sentence defining initial configurations, F ⊆ Q is the set of predicates denoting final states and ∆ is a set of transition rules. A transition rule is of the form q(y 1 , . . . , y #(q) ) a(X) ---→ ψ, where q ∈ Q is a predicate, a ∈ Σ is an input event and ψ ∈ Form + (Q, X ∪ {y 1 , . . . , y #(q) }) is a positive formula, where X ∩ {y 1 , . . . , y #(q) } = ∅. Without loss of generality, we consider, for each predicate q ∈ Q and each input event a ∈ Σ, at most one such rule, as two or more rules can be joined using disjunction. The quantifiers occurring in the right-hand side formula of a transition rule are called transition quantifiers. The size of A is

|A| def = |ι| + {|ψ| | q(y) a(X) ---→ ψ ∈ ∆}.
The semantics of first-order alternating automata is analogous to the semantics of propositional alternating automata, with rules of the form q a -→ φ, where q is a propositional variable and φ a positive boolean combination of propositional variables. For instance, q 0 a -→ (q 1 ∧ q 2 ) ∨ q 3 means that the automaton can choose to transition in either both q 1 and q 2 or in q 3 alone. This leads to defining transitions as the minimal models of the right hand side of a rule1 . The original definition of alternating automata [START_REF] Chandra | Alternation[END_REF] works around this problem and considers boolean valuations instead of formulae. In contrast, a finite description of a first-order alternating automaton cannot be given in terms of interpretations, as a first-order formula may have infinitely many models, corresponding to infinitely many initial or successor states occurring within an execution step.

Given an uninterpreted predicate symbol q ∈ Q and data values d 1 , . . . , d #(q) ∈ D, the tuple (q, d 1 , . . . , d #(q) ) is called a configuration, sometimes written q(d 1 , . . . , d #(q) ), when no confusion arises. A configuration is final if q ∈ F. An interpretation I corresponds to a set of configurations c(I)

def = {(q, d 1 , . . . , d #(q) ) | q ∈ Q, (d 1 , . . . , d #(q) ) ∈ q I }, called a cube.
This notation is lifted to sets of configurations in the usual way.

Definition 1. Given a word w = (a 1 , ν 1 ) . . . (a n , ν n ) ∈ Σ[X] * and a cube c, an execution of A = Σ, X, Q, ι, F, ∆ over w, starting with c, is a forest T = {T 1 , T 2 , . . .},
where each T i is a tree labeled with configurations, such that:

1. c = {T ( ) | T ∈ T } is the set of configurations labeling the roots of T 1 , T 2 , . . . and 2. if (q, d 1 , . . . , d #(q) ) labels a node on the level j ∈ [n -1] in T i , then the labels of its children form a cube from c(

[[ψ]] µ η ), where η = ν j+1 [y 1 ← d 1 , . . . , y #(q) ← d #(q)
] and q(y 1 , . . . , y #(q) ) a j+1 (X)

-----→ ψ ∈ ∆ is a transition rule of A.

An execution T over w, starting with c, is accepting if and only if all paths in T have the same length and the frontier of each tree T ∈ T is labeled with final configurations. If A has an accepting execution over w starting with a cube c ∈ c([[ι]] µ ), then A accepts w and let L(A) be the set of words accepted by A. For example, consider the automaton A = {a}, {x}, {q 0 , q 1 , q 2 , q f }, q 0 (0), {q f }, ∆ , where ∆ is the set: q 0 (y)

a(x) --→ q 1 (y+ x)∧q 2 (y- x), q 1 (y) a(x) --→ q 1 (y + x) ∨ (y > 0 ∧ q f ) and q 2 (y) a(x) --→ q 2 (y -x) ∨ (y > 0 ∧ q f ).
A possible execution tree of this automaton is the following:

(q 2 , -10)

(q 1 , 1) (q 1 , 3) q f (q 1 , 6) (q 1 , 10) (q 0 , 0) a, {x ← 1} a, {x ← 2} a, {x ← 3} a, {x ← 4} a, {x ← 5} (q 2 , -6) (q 2 , -1) (q 2 , -3) (q 2 , -15)
The execution tree is not accepting, since its frontier is not labeled with final configurations everywhere. Incidentally, here we have L(A) = ∅, which is proved by our tool in ∼ 0.5 seconds on an average machine.

In the rest of this paper, we are concerned with the following problems: 1. boolean closure:

given automata A i = Σ, X, Q i , ι i , F i , ∆ i , for i = 1, 2, do there exist automata A ∩ , A ∪ and A 1 such that L(A ∩ ) = L(A 1 ) ∩ L(A 2 ), L(A ∪ ) = L(A 1 ) ∪ L(A 2 ) and L(A 1 ) = Σ[X] * \ L(A 1 ) ? 2. emptiness: given an automaton A, is L(A) = ∅ ?
For technical reasons, we address the following problem next: given an automaton A and an input sequence α ∈ Σ * , does there exists a word w ∈ L(A) such that w Σ = α ? By solving this problem first, we develop the machinery required to prove that first-order alternating automata are closed under complement and, further, set up the ground for developping a practical semi-algorithm for the emptiness problem.

Path Formulae

In the upcoming developments it is sometimes more convenient to work with logical formulae defining executions of automata, than with low-level execution forests. For this reason, we first introduce path formulae Θ(α), which are formulae defining the executions of an automaton, over words that share a given sequence α of input events. Second, we restrict a path formula Θ(α) to an acceptance formula Υ(α), which defines only those executions that are accepting among Θ(α). Consequently, the automaton accepts a word w such that w Σ = α if and only if Υ(α) is satisfiable.

Let A = Σ, X, Q, ι, F, ∆ be an automaton for the rest of this section. For any i ∈ N, we denote by

Q (i) = {q (i) | q ∈ Q} and X (i) = {x (i) | x ∈ X}
the sets of time-stamped predicate symbols and variables, respectively. We also define

Q (≤n) def = {q (i) | q ∈ Q, i ∈ [n]} and
X (≤n) def = {x (i) | x ∈ X, i ∈ [n]}. For a formula ψ and i ∈ N, we define ψ (i) def = ψ[X (i) /X, Q (i)
/Q] the formula in which all input variables and state predicates (and only those symbols) are replaced by their time-stamped counterparts. Moreover, we write q(y) for q(y 1 , . . . , y #(q) ), when no confusion arises.

Given a sequence of input events α = a 1 . . . a n ∈ Σ * , the path formula of α is:

Θ(α) def = ι (0) ∧ n i=1 q(y) a i (X)
---→ψ∈∆ ∀y 1 . . . ∀y #(q) . q (i-1) (y) → ψ (i) (

The automaton A, to which Θ(α) refers, will always be clear from the context. To formalize the relation between the low-level configuration-based execution semantics and path formulae, consider a word w = (a 1 , ν 1 ) . . . (a n , ν n ) ∈ Σ[X] * . Any execution T of A over w has an associated interpretation I T of time-stamped predicates Q (≤n) :

I T (q (i) ) def = {(d 1 , . . . , d #(q) ) | (q, d 1 , . . . , d #(q) ) labels a node on level i in T }, ∀q ∈ Q ∀i ∈ [n] Lemma 1. Given an automaton A = Σ, X, Q, ι, F, ∆ , for any word w = (a 1 , ν 1 ) . . . (a n , ν n ), we have [[Θ(w Σ )]] µ w D = {I T |
T is an execution of A over w}. Next, we give a logical characterization of acceptance, relative to a given sequence of input events α ∈ Σ * . To this end, we constrain the path formula Θ(α) by requiring that only final states of A occur on the last level of the execution. The result is the acceptance formula for α:

Υ(α) def = Θ(α) ∧ q∈Q\F ∀y 1 . . . ∀y #(q) . q (n) (y) → ⊥ (2)
The top-level universal quantifiers from a subformula ∀y 1 . . . ∀y #(q) . q (i) (y) → ψ of Υ(α) will be referred to as path quantifiers, in the following. Notice that path quantifiers are distinct from the transition quantifiers that occur within a formula ψ of a transition rule q(y 1 , . . . , y #(q) ) a(X)

---→ ψ of A. The relation between the words accepted by A and the acceptance formula above, is formally captured by the following lemma: Lemma 2. Given an automaton A = Σ, X, Q, ι, F, ∆ , for every word w ∈ Σ[X] * , the following are equivalent: (1) there exists an interpretation I such that I, w D | = Υ(w Σ ) and (2) w ∈ L(A).

As an immediate consequence, one can decide whether A accepts some word w with a given input sequence w Σ = α, by checking whether Υ(α) is satisfiable. However, unlike non-alternating infinite-state models of computation, such as counter automata (nondeterministic programs with integer variables), the satisfiability query for an acceptance (path) formula falls outside of known decidable theories, supported by standard SMT solvers. There are basically two reasons for this, namely (i) the presence of predicate symbols, and (ii) the non-trivial alternation of quantifiers. To understand this point, consider for example, the decidable theory of Presburger arithmetic [START_REF] Presburger | Über die Vollstandigkeit eines gewissen Systems der Arithmetik[END_REF]. Adding even only one monadic predicate symbol to it yields undecidability in the presence of non-trivial quantifier alternation [START_REF] Halpern | Presburger arithmetic with unary predicates is π 1 1 complete[END_REF]. On the other hand, the quantifier-free fragment of Presburger arithmetic extended with uninterpreted function symbols is decidable, by a Nelson-Oppen style congruence closure argument [START_REF] Nelson | Fast decision procedures based on congruence closure[END_REF].

To tackle the problem of deciding satisfiability of Υ(α) formulae, we start from the observation that their form is rather particular, which allows the elimination of path quantifiers and uninterpreted predicate symbols, by a couple of satisfiability-preserving transformations. The result of applying these transformations is a formula with no predicate symbols, whose only quantifiers are those introduced by the transition rules of the automaton. Next, in §3 we shall assume moreover that the first-order theory of the data sort D (without uninterpreted predicate symbols) has quantifier elimination, providing thus an effective decision procedure.

For the time being, let us formally define the elimination of transition quantifiers and predicate symbols. Let α = a 1 . . . a n be a given sequence of input events and let α i be the prefix a 1 . . . a i of α, for i ∈ [n], where α 0 = . We consider the sequence of formulae Θ(α 0 ), . . . , Θ(α n ) defined as Θ(α 0 ) def = ι (0) and, for all i ∈ [1, n], let Θ(α i ) be the conjunction of Θ(α i-1 ) with all formulae q (i-1) (t 1 , . . . , t #(q) ) → ψ (i) [t 1 /y 1 , . . . , t #(q) /y #(q) ], such that q (i-1) (t 1 , . . . , t #(q) ) occurs in Θ(α i-1 ), for some terms t 1 , . . . , t #(q) . Next, we write Υ(α) for the conjunction of Θ(α n ) with all q (n) (t 1 , . . . , t #(q) ) → ⊥, such that q (n) (t 1 , . . . , t #(q) ) occurs in Θ(α n ), for some q ∈ Q \ F. Note that Υ(α) contains no path quantifiers, as required. On the other hand, the scope of the transition quantifiers in Υ(α) exceeds the right-hand side formulae from the transition rules, as shown by the following example.

Example 1. Consider the automaton

A = {a 1 , a 2 }, {x}, {q, q f }, ι, {q f }, ∆ , where: ι = ∃z . z ≥ 0 ∧ q(z) ∆ = {q(y) a 1 (x) ---→ x ≥ 0 ∧ ∀z . z ≤ y → q(x + z), q(y) a 2 (x)
---→ y < 0 ∧ q f (x + y)} For the input event sequence α = a 1 a 2 , the acceptance formula is:

Υ(α) = ∃z 1 . z 1 ≥ 0 ∧ q (0) (z 1 ) ∧ ∀y . q (0) (y) → [x (1) ≥ 0 ∧ ∀z 2 . z 2 ≥ y → q (1) (x (1) + z 2 )] ∧ ∀y . q (1) (y) → [y < 0 ∧ q f (2) (x (2) + y)]
The result of eliminating the path quantifiers, in prenex normal form, is shown below:

Υ(α) = ∃z 1 ∀z 2 . z 1 ≥ 0 ∧ q (0) (z 1 ) ∧ [q (0) (z 1 ) → x (1) ≥ 0 ∧ (z 2 ≥ z 1 → q (1) (x (1) + z 2 ))] ∧ [q (1) (x (1) + z 2 ) → x (1) + z 2 < 0 ∧ q f (2) (x (2) + x (1) + z 2 )]
Notice that the transition quantifiers ∃z 1 and ∀z 2 from Υ(α) range now over Υ(α). Further, we eliminate the predicate atoms from Υ(α), by considering the sequence of formulae Θ(α 0 ) def = ι (0) and Θ(α i ) is obtained by substituting each predicate atom q (i-1) (t 1 , . . . , t #(q) ) in Θ(α i-1 ) by ψ (i) [t 1 /y 1 , . . . , t #(q) /y #(q) ], where q(y)

a i (X) ---→ ψ ∈ ∆, for all i ∈ [1, n].
We write Υ(α) for the formula obtained by replacing, in Θ(α), each occurrence of a predicate q (n) , such that q ∈ Q \ F (resp. q ∈ F), by ⊥ (resp. ).

Example 2 (Contd. from Example 1). The result of the elimination of predicate atoms from the acceptance formula in Example 1 is shown below:

Υ(α) = ∃z 1 ∀z 2 . z 1 ≥ 0 ∧ [x (1) ≥ 0 ∧ (z 2 ≥ z 1 → x (1) + z 2 < 0)
] Since this formula is unsatisfiable, by Lemma 5 below, no word w with input event sequence w Σ = a 1 a 2 is accepted by the automaton A from Example 1.

At this point, we prove the formal relation between the satisfiability of the formulae Υ(α) and Υ(α). Since there are no occurrences of predicates in Υ(α), for each valuation ν : X (≤n) → D, there exists an interpretation I such that I, ν | = Υ(α) if and only if J, ν | = Υ(α), for every interpretation J. In this case we omit I and simply write ν | = Υ(α). Finally, we define the acceptance of a word with a given input event sequence by means of a quantifier-free formula in which no predicate atom occurs.

Lemma 5. Given an automaton A = Σ, X, Q, ι, F, ∆ , for every word w ∈ Σ[X] * , we have w D | = Υ(w Σ ) if and only if w ∈ L(A).

Boolean Closure of First Order Alternating Automata

Given a positive formula φ, we define the dual formula φ ∼ recursively as follows:

(φ 1 ∨ φ 2 ) ∼ def = φ 1 ∼ ∧ φ 2 ∼ (φ 1 ∧ φ 2 ) ∼ def = φ 1 ∼ ∨ φ 2 ∼ (t = s) ∼ def = t s (∃x . φ 1 ) ∼ def = ∀x . φ 1 ∼ (∀x . φ 1 ) ∼ def = ∃x . φ 1 ∼ (t s) ∼ def = t = s q(x 1 , . . . , x #(q) ) ∼ def = q(x 1 , . . . , x #(q) )
The following theorem shows closure of automata under all boolean operations. Note that it is sufficient to show closure under intersection and negation because L(A 1 ) ∪ L(A 2 ) is the complement of the language L c (A 1 ) ∩ L c (A 2 ), for any two automata A 1 and A 2 with the same input event alphabet and set of input variables.

Theorem 1. Given automata

A i = Σ, X, Q i , ι i , F i , ∆ i , for i = 1, 2, such that Q 1 ∩ Q 2 = ∅, the following hold: 1. L(A ∩ ) = L(A 1 ) ∩ L(A 2 ), where A ∩ = Σ, X, Q 1 ∪ Q 2 , ι 1 ∧ ι 2 , F 1 ∪ F 2 , ∆ 1 ∪ ∆ 2 , 2. L(A i ) = Σ[X] * \ L(A i ), where A i = Σ, X, Q i , ι ∼ , Q i \ F i , ∆ ∼ i and ∆ ∼ i = {q(y) a(X) ---→ ψ ∼ | q(y) a(X) ---→ ψ ∈ ∆ i }, for i = 1, 2. Moreover, |A ∩ | = O(|A 1 | + |A 2 |) and |A i | = O(|A i |), for i = 1, 2.

The Emptiness Problem

The emptiness problem is undecidable even for automata with predicates of arity two, whose transition rules use only equalities and disequalities, having no transition quantifiers [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF]. Since even such simple classes of alternating automata have no general decision procedure for emptiness, we use an abstraction-refinement semi-algorithm based on lazy annotation [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF][START_REF] Mcmillan | Lazy annotation revisited[END_REF]. In a nutshell, a lazy annotation procedure systematically explores the set of finite input event sequences searching for an accepting execution. For an input sequence, if the path formula is satisfiable, we compute a word in the language of the automaton, from the model of the path formula. Otherwise, i.e. the sequence is spurious, the search backtracks and each position in the sequence is annotated with an interpolant, thus marking the sequence as infeasible. The semi-algorithm uses moreover a coverage relation between sequences, ensuring that the continuations of already covered sequences are never explored. Sometimes this coverage relation provides a sound termination argument, in case when the automaton is empty.

For two input event sequences α, β ∈ Σ * , we say that α is a prefix of β, written α β, if α = βγ for some sequence γ ∈ Σ * . A set S of sequences is prefix-closed if for each α ∈ S , if β α then β ∈ S , and complete if for each α ∈ S , there exists a ∈ Σ such that αa ∈ S if and only if αb ∈ S for all b ∈ Σ. A prefix-closed set is the backbone of a tree whose edges are labeled with input events. If the set is, moreover, complete, then every node of the tree has either zero successors, in which case it is called a leaf, or it has a successor edge labeled with a for each input event a ∈ Σ. Definition 2. An unfolding of an automaton A = Σ, X, Q, ι, F, ∆ is a finite partial mapping U : Σ * fin Form + (Q, ∅), whose domain dom(U) is a finite prefix-closed complete set, such that U( ) = ι, and for each sequence αa ∈ dom(U), such that α ∈ Σ * and a ∈ Σ:

U(α) (0) ∧ q(y) a(X)
---→ψ ∀y 1 . . . ∀y #q . q (0) (y) → ψ (1) | = U(αa) (1) A path α is safe in U if and only if U(α)∧ q∈Q\F ∀y 1 . . . ∀ y #(q) . q(y) → ⊥ is unsatisfiable. The unfolding U is safe if and only if every path in dom(U) is safe in U.

Lazy annotation semi-algorithms [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF][START_REF] Mcmillan | Lazy annotation revisited[END_REF] build unfoldings of automata trying to discover counterexamples for emptiness. If the automaton A in question is non-empty, a systematic enumeration of the input event sequences2 from Σ * will suffice to discover a word w ∈ L(A), provided that the first-order theory of the data domain D is decidable (Lemma 2). However, if L(A) = ∅, the enumeration of input event sequences may, in principle, run forever. The typical way of fighting this divergence problem is to define a coverage relation between the nodes of the unfolding tree.

Algorithm 1 IMPACT-based Semi-algorithm for First Order Alternating Automata

input: a first order alternating automaton A = Σ, X, Q, ι, F, ∆ output: if L(A) = ∅, or word w ∈ L(A), otherwise data structures: WorkList and unfolding tree U = N, E, r, U, , where:

-N is a set of nodes, -E ⊆ N × Σ × N is a set of edges labeled by input events, -U :

N → Form + (Q, ∅) is a labeling of nodes with positive sentences -⊆ N × N is a coverage relation, initially WorkList = {r} and N = E = U = = ∅. 1: while WorkList ∅ do 2:
dequeue n from WorkList 3:

N ← N ∪ {n} 4:
let α(n) be a 1 , . . . , a k 5:

if Υ(α)(X (1) , . . . , X (k) ) is satisfiable then counterexample is feasible 6:

get model ν of Υ(α)(X (1) , . . . , X (k) ) 7:

return w = (a 1 , ν(X (1) )) . . . (a k , ν(X (k) )) w ∈ L(A) by construction 8:

else spurious counterexample 9: let (I 0 , . . . , I k ) be a GLI for α 10:

b ← ⊥ 11: A lazy annotation semi-algorithm will stop and report emptiness provided that it succeeds in building a closed and safe unfolding of the automaton. Notice that, by Definition 3, for any three nodes of an unfolding U, say α, β, γ ∈ dom(U), if α ≺ β and α γ, then β γ as well. As we show next (Theorem 2), there is no need to expand covered nodes, because, intuitively, there exists a word w ∈ L(A) such that α w Σ and α γ only if there exists another word u ∈ L(A) such that γ u Σ . Hence, exploring only those input event sequences that are continuations of γ (and ignoring those of α) suffices in order to find a counterexample for emptiness, if one exists.

for i = 0, . . . , k do 12: if U(n i ) | = I i then 13: Uncover ← {m ∈ N | (m, n i ) ∈ } 14: ← \ {(m, n i ) | m ∈
for y ∈ N such that α(y) ≺ * α(x) do 29: if U(x) | = U(y) then 30: ← \ {(p, q) ∈ | q is x
An unfolding node α ∈ dom(U) is said to be spurious if and only if Υ(α) is unsatisfiable. In this case, we change (refine) the labels of (some of the) prefixes of α (and that of α), such that U(α) becomes ⊥, thus indicating that there is no real execution of the automaton along that input event sequence. As a result of the change of labels, if a node γ α used to cover another node from dom(U), it might not cover it with the new label. Therefore, the coverage relation has to be recomputed after each refinement of the labeling. The semi-algorithm stops when (and if) a safe complete unfolding has been found.

Theorem 2. If an automaton A has a nonempty safe closed unfolding then

L(A) = ∅.
We describe the semi-algorithm used to check emptiness of first-order alternating automata. The execution of Algorithm 1 consists of three phases, corresponding to the Close, Refine and Expand of the original IMPACT procedure [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF]. Let n be a node removed from the worklist at line 2 and let α(n) be the input sequence labeling the path from the root node to n. If Υ(α(n)) is satisfiable, the sequence α(n) is feasible, in which case a model of Υ(α(n)) is obtained and a word w ∈ L(A) is returned. Otherwise, α(n) is an infeasible input sequence and the procedure enters the refinement phase (lines 9-19). The GLI for α(n) is used to strenghten the labels of all the ancestors of n, by conjoining the formulae of the interpolant, changed according to Lemma 7, to the existing labels.

In this process, the nodes on the path between r and n, including n, might become eligible for coverage, therefore we attempt to close each ancestor of n that is impacted by the refinement (line [START_REF] Lyndon | An interpolation theorem in the predicate calculus[END_REF]. Observe that, in this case the call to Close must uncover each node which is covered by a successor of n (line 30 of the Close function). This is required because, due to the over-approximation of the sets of reachable configurations, the covering relation is not transitive, as explained in [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF]. If Close adds a covering edge (n i , m) to , it does not have to be called for the successors of n i on this path, which is handled via the boolean flag b. Finally, if n is still uncovered (it has not been previously covered during the refinement phase) we expand n (lines 21-25) by creating a new node for each successor s via the input event a ∈ Σ and inserting it into the worklist.

Interpolant Generation

Typically, when checking the unreachability of a set of program configurations, the interpolants used to annotate the unfolded control structure are assertions about the values of the program variables in a given control state, at a certain step of an execution [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF]. Because we consider alternating computation trees (forests), we must distinguish between (i) locality of interpolants w.r.t. a given control state (control locality) and (ii) locality w.r.t. a given time stamp (time locality). In logical terms, control-local interpolants are formulae involving a single predicate symbol, whereas time-local interpolants involve only predicates q (i) and variables x (i) , for a single i ≥ 0. When considering alternating executions, control-local interpolants are not always enough to prove emptiness, because of the synchronization of several branches of the computation on the same input word. For this reason, the interpolants considered in this paper will never be control-local and we shall use the term local to denote time-local interpolants, with no free variables.

First, let us give the formal definition of the class of interpolants we shall work with. Given a formula φ, the vocabulary of φ, denoted V(φ) is the set of predicate symbols q ∈ Q (i) and variables x ∈ X (i) , occurring in φ, for some i ≥ 0. For a term t, its vocabulary V(t) is the set of variables that occur in t. Observe that quantified variables and the interpreted function symbols of the data theory 3 do not belong to the vocabulary of a formula. By P + (φ) [P -(φ)] we denote the set of predicate symbols that occur in φ under an even [odd] number of negations.

Definition 4 ([19]

). Given formulae φ and ψ such that φ ∧ ψ is unsatisfiable, a Lyndon interpolant is a formula I such that φ | = I, the formula I ∧ ψ is unsatisfiable,

V(I) ⊆ V(φ) ∩ V(ψ), P + (I) ⊆ P + (φ) ∩ P + (ψ) and P -(I) ⊆ P -(φ) ∩ P -(ψ).
In the rest of this section, fix an automaton A = Σ, X, Q, ι, F, ∆ . The following definition generalizes interpolants from unsatisfiable conjunctions to input sequences: Definition 5. Given a sequence of input events α = a 1 . . . a n ∈ Σ * , a generalized Lyndon interpolant (GLI) is a sequence (I 0 , . . . , I n ) of formulae such that, for all k ∈ [n -1], the following hold: (1)

P -(I k ) = ∅, (2) ι (0) | = I 0 , I k ∧ q(y) a i (X)
---→ψ∈∆ ∀y 1 . . . ∀y #(q) . q (k) (y) → ψ (k+1) | = I k+1 and (3) I n ∧ q∈Q\F ∀y 1 . . . ∀y #(q) . q(y) → ⊥ is unsatisfiable. Moreover, the GLI is local if and only if

V(I k ) ⊆ Q (k) , for all k ∈ [n].
The following proposition states the existence of local GLI for the theories in which Lyndon's Interpolation Theorem holds.

Proposition 1. If there exists a Lyndon interpolant for any two formulae φ and ψ, in the first-order theory of data with uninterpreted predicate symbols, such that φ ∧ ψ is unsatisfiable, then any sequence of input events α = a 1 . . . a n ∈ Σ * , such that Υ(α) is unsatisfiable, has a local GLI (I 0 , . . . , I n ).

A problematic point of the above proposition is that the existence of Lyndon interpolants (Definition 4) is proved in principle, but the proof is non-constructive. In other words, the proof of Proposition 1 does not yield an algorithm for computing GLIs, for the following reason. Building an interpolant for an unsatisfiable conjunction of formulae φ ∧ ψ is typically the job of the decision procedure that proves the unsatisfiability and, in general, there is no such procedure, when φ and ψ contain predicates and have non-trivial quantifier alternation. In this case, some provers use instantiation heuristics for the universal quantifiers that are sufficient for proving unsatisfiability, however these heuristics are not always suitable for interpolant generation. Consequently, from now on, we assume the existence of an effective Lyndon interpolation procedure only for decidable theories, such as the quantifier-free linear (integer) arithmetic with uninterpreted functions (UFLIA, UFLRA, etc.) [START_REF] Rybalchenko | Constraint solving for interpolation[END_REF]. This is where the predicate-free path formulae (defined in §2.1) come into play. Recall that, for a given event sequence α, the automaton A accepts a word w such that w Σ = α if and only if Υ(α) is satisfiable (Lemma 5). Assuming further that the equality and interpreted predicates (e.g. inequalities for integers) atoms from the transition rules of A belong to a decidable first-order theory, such as Presburger arithmetic, Lemma 5 gives us an effective way of checking emptiness of A, relative to a given event sequence. However, this method does not cope well with lazy annotation, because there is no way to extract, from the unsatisfiability proof of Υ(α), the interpolants needed to annotate α. This is because (I) the formula Υ(α), obtained by repeated substitutions loses track of the steps of the execution, and (II) quantifiers that occur nested in Υ(α) make it difficult to write Υ(α) as an unsatisfiable quantifier-free conjunction of formulae from which interpolants are extracted (Definition 4).

The solution we adopt for the first issue (I) consists in partially recovering the timestamped structure of the acceptance formula Υ(α) using the formula Υ(α), in which only transition quantifiers occur. The second issue (II) is solved under the additional assuption that the theory of the data domain D has witness-producing quantifier elimination. More precisely, we assume that, for each formula ∃x . φ(x), there exists an effectively computable term τ, in which x does not occur, such that ∃x . φ and φ[τ/x] are equisatisfiable. These terms, called witness terms in the following, are actual definitions of the Skolem function symbols from the following folklore theorem: Theorem 3 ( [START_REF] Börger | The Classical Decision Problem[END_REF]). Given Q 1 x 1 . . . Q n x n . φ a first-order sentence, where Q 1 , . . . , Q n ∈ {∃, ∀} and φ is quantifier-free, let η i def = f i (y 1 , . . . ,

y k i ) if Q i = ∀ and η i def = x i if Q i = ∃,
where f i is a fresh function symbol and {y 1 , . . . ,

y k i } = {x j | j < i, Q j = ∃}. Then the entailment Q 1 x 1 . . . Q n x n . φ | = φ[η 1 /x 1 , . . . , η n /x n ] holds.
Examples of witness-producing quantifier elimination procedures can be found in the literature for e.g. linear integer (real) arithmetic (LIA,LRA), Presburger arithmetic and boolean algebra of sets and Presburger cardinality constraints (BAPA) [START_REF] Kuncak | Software synthesis procedures[END_REF].

Under the assumption that witness terms can be effectively built, we describe the generation of a non-local GLI for a given input event sequence α = a 1 . . . a n . First, we generate successively the acceptance formula Υ(α) and its equisatisfiable forms

Υ(α) = Q 1 x 1 . . . Q m x m . Φ and Υ(α) = Q 1 x 1 . . . Q m x m . Φ,
both written in prenex form, with matrices Φ and Φ, respectively. Because we assumed that the first order theory of D has quantifier elimination, the satisfiability problem for Υ(α) is decidable. If Υ(α) is satisfiable, we build a counterexample for emptiness w such that w Σ = α and w D is a satisfying assignment for Υ(α). Otherwise, Υ(α) is unsatisfiable and there exist witness terms τ i 1 . . . τ i , where {i 1 , . . .

, i } = { j ∈ [1, m] | Q j = ∀}, such that Φ[τ i 1 /x i 1 , . . . , τ i /x i ]
is unsatisfiable (Theorem 3). Then it turns out that the formula Φ[τ i 1 /x i 1 , . . . , τ i /x i ], obtained analogously from the matrix of Υ(α), is unsatisfiable as well (Lemma 6 below). Because this latter formula is structured as a conjunction of formulae ι (0) ∧φ 1 . . .∧φ n ∧ψ, where ) , it is now possible to use an existing interpolation procedure for the quantifier-free theory of D, extended with uninterpreted function symbols, to compute a (not necessarily local) GLI (I 0 , . . . ,

V(φ k ) ∩ Q (≤n) ⊆ Q (k-1) ∪ Q (k) and V(ψ) ∩ Q (≤n) ⊆ Q (n
I n ) such that V(I k ) ∩ Q (≤n) ⊆ Q (k) , for all k ∈ [n].
Example 3 (Contd. from Examples 1 and 2). The formula Υ(α) (Example 2) is unsatisfiable and let τ 2 def = z 1 be the witness term for the universally quantified variable z 2 . Replacing z 2 with τ 2 (z 1 ) in the matrix of Υ(α) (Example 1) yields the unsatisfiable conjunction below, obtained after trivial simplifications:

[z 1 ≥ 0 ∧ q (0) (z 1 )] ∧ [q (0) (z 1 ) → x (1) ≥ 0 ∧ q (1) (x (1) + z 1 )] ∧ [q (1) (x (1) + z 1 ) → x (1) + z 1 < 0 ∧ q f (2) (x (2) + x (1) + z 1 )] A non-local GLI for the above conjunction is the sequence of formulae:

(q (0) (z 1 ) ∧ z 1 ≥ 0, x (1) ≥ 0 ∧ q (1) (x (1) + z 1 ) ∧ z 1 ≥ 0, ⊥)

We formalize and prove the correctness for the above construction of non-local GLI. A function ξ : N → N is monotonic iff for each n < m we have ξ(n) ≤ ξ(m) and finiterange iff for each n ∈ N the set {m | ξ(m) = n} is finite. If ξ is finite-range, we denote by ξ -1 max (n) ∈ N the maximal value m such that ξ(m) = n.

Lemma 6. Given a non-empty input event sequence α = a 1 . . .

a n ∈ Σ * , such that Υ(α) is unsatisfiable, let Q 1 x 1 . . . Q m x m . Φ be a prenex form of Υ(α) and let ξ : [1, m] → [n]
be a monotonic finite-range function mapping each transition quantifier to the minimal index from the sequence Θ(α 0 ), . . . , Θ(α n ) where it occurs. Then one can effectively build: 1. witness terms τ i 1 , . . . , τ i , where {i 1 , . . .

, i } = { j ∈ [1, m] | Q j = ∀} and V(τ i j ) ⊆ X (≤ξ(i j )) ∪ {x k | k < i j , Q k = ∃}, ∀ j ∈ [1, ] such that Φ[τ i 1 /x i 1 , . . . , τ i /x i ]
is unsatisfiable, and 2. a GLI (I 0 , . . . , I n ) for α, such that

V(I k ) ⊆ Q (k) ∪ X (≤k) ∪ {x j | j < ξ -1 max (k), Q j = ∃}, for all k ∈ [n].
Consequently, under two assumptions about the first-order theory of the data domain, namely (i) witness-producing quantifier elimination, and (ii) Lyndon interpolation for the quantifier-free fragment with uninterpreted functions, we developed a generic method that produces GLIs for unfeasible input event sequences. Moreover, each formula in the interpolant refers only to the current predicate symbols, the current and past input variables and the existentially quantified transition variables introduced at the previous steps. The remaining questions are how to use these GLIs to label the sequences in the unfolding of an automaton (Definition 2) and compute coverage (Definition 3) between nodes of the unfolding.

Unfolding with Non-local Interpolants

As required by Definition 2, the unfolding U of an automaton A = Σ, X, Q, ι, F, ∆ is labeled by formulae U(α) ∈ Form + (Q, ∅), with no free symbols, other than predicate symbols, such that the labeling is compatible with the transition relation of the automaton. Each newly expanded input sequence of A is initially labeled with and the labels are refined using GLIs computed from proofs of spuriousness. The following lemma describes the refinement of the labeling of an input sequence by a non-local GLI: Lemma 7. Let U be an unfolding of an automaton A = Σ, X, Q, ι, F, ∆ such that α = a 1 . . . a n ∈ dom(U) and (I 0 , . . . , I n ) is a GLI for α. Then the mapping U : dom(U) → Form + (Q, ∅) is an unfolding of A, where:

-

U (α k ) = U(α k ) ∧ J k , for all k ∈ [n]
, where J k is the formula obtained from I k by removing the time stamp of each predicate symbol q (k) and existentially quantifying each free variable, and

-U (β) = U(β) if β ∈ dom(U) and β α, Moreover, α is safe in U .
Observe that, by Lemma 6 (2), the set of free variables of a GLI formula I k consists of (i) variables X (≤k) keeping track of data values seen in the input at some earlier moment in time, and (ii) variables that track past choices made within the transition rules. Basically, it is not important when exactly in the past a certain input has been read or when a choice has been made, because only the relation between the values of these and the current variables determines the future behavior of the automaton. Quantifying these variables existentially does the job of ignoring when exactly in the past these values have been seen. Moreover, the last point of Lemma 7 ensures that the refined path is safe in the new unfolding and will stay safe in all future refinements of this unfolding.

The last ingredient of the lazy annotation semi-algorithm based on unfoldings consist in the implementation of the coverage check, when the unfolding of an automaton is labeled with conjunctions of existentially quantified formulae with predicate symbols, obtained from interpolation. By Definition 3, checking whether a given node α ∈ dom(U) is covered amounts to finding a prefix α α and a node β ∈ dom(U) such that U(α ) | = U(β), or equivalently, the formula U(α ) ∧ ¬U(β) is unsatisfiable. However, the latter formula, in prenex form, has quantifier prefix in the language ∃ * ∀ * and, as previously mentioned, the satisfiability problem for such formulae becomes undecidable when the data theory subsumes Presburger arithmetic [START_REF] Halpern | Presburger arithmetic with unary predicates is π 1 1 complete[END_REF].

Nevertheless, if we require just a yes/no answer (i.e. not an interpolant) recently developed quantifier instantiation heuristics [START_REF] Reynolds | Solving quantified linear arithmetic by counterexampleguided instantiation[END_REF] perform rather well in answering a large number of queries in this class. Observe, moreover, that coverage does not need to rely on a complete decision procedure. If the prover fails in answering the above satisfiability query, then the semi-algorithm assumes that the node is not covered and continues exploring its successors. Failure to compute complete coverage may lead to divergence (non-termination) and ultimately, to failure to prove emptiness, but does not affect the soundness of the semi-algorithm (real counterexamples will still be found).

Experimental Results

We have implemented a version of the IMPACT semi-algorithm [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF] in a prototype tool, avaliable online [START_REF]First Order Alternating Data Automata (FOADA[END_REF]. The tool is written in Java and uses the Z3 SMT solver [START_REF]Z3 SMT Solver[END_REF], via the JavaSMT interface [START_REF] Javasmt | [END_REF], for spuriousness and coverage queries and also for interpolant generation. Table 1 reports the size of the input automaton in bytes, the numbers of Predicates, Variables and Transitions, the result of emptiness check, the number of Expanded and Visited Nodes during the unfolding and the Time in miliseconds. The experiments were carried out on a MacOS x64 -1. The test cases shown in Table 1, come from several sources, namely predicate automata models (*.pa) [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF] available online [START_REF]Predicate Automata[END_REF], timed automata inclusion problems (abp.ada, train.ada, rr-crossing.foada), array logic entailments (array rotation.ada, array simple.ada, array shift.ada) and hardware circuit verification (hw1.ada, hw2.ada), initially considered in [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF], with the restriction that local variables are made visible in the input. The train-simpleN. foada and fischer-mutexN. foada examples are parametric verification problems in which one checks inclusions of the form N i=1 L(A i ) ⊆ L(B), where A i is the i-th copy of the template automaton. The advantage of using FOADA over the INCLUDER [12] tool from [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] is the possibility of having automata over infinite alphabets with local variables, whose values are not visible in the input. In particular, this is essential for checking inclusion of timed automata that use internal clocks to control the computation.

Conclusions

We present first-order alternating automata, a model of computation that generalizes classical boolean alternating automata to first-order theories. Due to their expressivity, first-order alternating automata are closed under union, intersection and complement. However the emptiness problem is undecidable even in the most simple case, of the quantifier-free theory of equality with uninterpreted predicate symbols. We deal with the emptiness problem by developping a practical semi-algorithm that always terminates, when the automaton is not empty. In case of emptiness, termination of the semialgorithm occurs in most practical test cases, as shown by a number of experiments.

=

  {I | I, ν | = φ, ∀I ⊆ I . I , ν | = φ} the set of minimal interpretations that, together with ν, form models of φ.

Lemma 3 .

 3 For any input event sequence α = a 1 . . . a n and each valuation ν : X (≤n) → D, the following hold, for every interpretation I: (1) if I, ν | = Υ(α) then I, ν | = Υ(α), and (2) if I, ν | = Υ(α) there exists an interpretation J ⊆ I such that J, ν | = Υ(α).

Lemma 4 .

 4 For any input event sequence α = a 1 . . . a n and each valuation ν : X (≤n) → D, there exists a valuation I such that I, ν | = Υ(α) if and only if ν | = Υ(α).

Definition 3 .

 3 or a successor of x} ∪ {(x, Given an unfolding U of an automaton A = Σ, X, Q, ι, F, ∆ a node α ∈ dom(U) is covered by another node β ∈ dom(U), denoted α β, if and only if there exists a node α α such that U(α ) | = U(β). Moreover, U is closed if and only if every leaf from dom(U) is covered by an uncovered node.

Table 1 .

 1 3 GHz Intel Core i5 -8 GB 1867 MHz LPDDR3 machine. Example |A| (bytes) Predicates Variables Transitions L(A) = ∅ ? Nodes Expanded Nodes Visited Time (msec) Experiments with First Order Alternating Automata

	incdec.pa	499	3	1	12	no	21	17	779
	localdec.pa	678	4	1	16	no	49	35	1814
	ticket.pa	4250	13	1	73	no	229	91	9543
	count thread0.pa	9767	14	1	126	no	154	128	8553
	count thread1.pa	10925	15	1	135	no	766	692	76771
	local0.pa	10595	13	1	117	no	73	27	1431
	local1.pa	11385	14	1	126	no	1135	858	101042
	array rotation.ada	1834	8	7	7	yes	9	8	1543
	array simple.ada	3440	9	5	8	yes	11	10	6787
	array shift.ada	874	6	5	5	yes	6	5	413
	abp.ada	6909	16	14	28	no	52	47	4788
	train.ada	1823	10	4	26	yes	68	67	7319
	hw1.ada	322	3	2	5	Solver Error	/	/	/
	hw2.ada	674	7	2	8	yes	20	22	4974
	rr-crossing.foada	1780	10	1	16	yes	67	67	7574
	train-simple1.foada	5421	13	1	61	yes	43	44	2893
	train-simple2.foada	10177	16	1	118	yes	111	113	8386
	train-simple3.foada	15961	19	1	193	yes	196	200	15041
	fischer-mutex2.foada	3000	11	2	23	yes	23	23	808
	fischer-mutex3.foada	4452	16	2	34	yes	33	33	1154

Both {q 1 ← , q

← , q

← ⊥} and {q 1 ← ⊥, q 2 ← ⊥, q 3 ← } are minimal models, however {q 1 ← , q 2 ← , q 3 ← } is a model but is not minimal.

For instance, using breadth-first search.

E.g., the arithmetic operators of addition and multiplication, when D is the set of integers.