Mohammad Javad Amiri
email: 1mjamiri@seas.upenn.edu

Tristan Allard
email: tristan.allard@irisa.fr3agrawal

Divyakant Agrawal

Amr El Abbadi

PReVer: Towards Private Regulated Verified Data

Data privacy has garnered significant attention recently due to diverse applications that store sensitive data in untrusted infrastructure. From a data management point of view, the focus has been on the privacy of stored data and the privacy of querying data at a large scale. However, databases are not solely query engines on static data, they must support updates on dynamically evolving datasets. In this paper, we lay out a vision for privacy-preserving dynamic data. In particular, we focus on dynamic data that might be stored remotely on untrusted providers. Updates arrive at a provider and are verified and incorporated into the database based on predefined constraints. Depending on the application, the content of the stored data, the content of the updates and the constraints may be private or public. We then propose PReVer, a universal framework for managing regulated dynamic data in a privacy-preserving manner. We explore a set of research challenges that PReVer needs to address in order to guarantee the privacy of data, updates, and/or constraints and address the consistent and verifiable execution of updates. This opens the space of privacy-preserving data management from the narrow perspective of private queries on static datasets to the larger space of private management of dynamic data.

INTRODUCTION

Data privacy 1 has garnered significant attention recently due to diverse applications that store sensitive data in untrusted infrastructure. Data privacy and enabling secure query processing on data using cryptographic techniques have been addressed in several systems [START_REF] Agarwal | Encrypted databases for differential privacy[END_REF][START_REF] Arasu | Oblivious query processing[END_REF][START_REF] Bater | Shrinkwrap: efficient sql query processing in differentially private data federations[END_REF][START_REF] Bellare | Deterministic and efficiently searchable encryption[END_REF][START_REF] Chen | Pegasus: Data-adaptive differentially private stream processing[END_REF][START_REF] Dwork | Differential privacy under continual observation[END_REF][START_REF] Hacigümüş | Executing SQL over encrypted data in the database-service-provider model[END_REF][START_REF] Hore | Secure multidimensional range queries over outsourced data[END_REF][START_REF] Kellaris | Accessing data while preserving privacy[END_REF][START_REF] Li | Prism: Private Verifiable Set Computation over Multi-Owner Outsourced Databases[END_REF][START_REF] Poddar | Arx: A Strongly Encrypted Database System[END_REF][START_REF] Roy Chowdhury | Crypt𝜖: Crypto-assisted differential privacy on untrusted servers[END_REF][START_REF] Cetin Sahin | A Differentially Private Index for Range Query Processing in Clouds[END_REF]. As an example, Prism [START_REF] Li | Prism: Private Verifiable Set Computation over Multi-Owner Outsourced Databases[END_REF] presents a secret-sharing-based technique to answer queries in the form of private set operations as well as aggregation functions over outsourced databases belonging to multiple owners. The focus of such private database systems, however, is mainly on static databases and they do not support updates on dynamically evolving databases in a satisfactory manner [START_REF] Wang | DP-Sync: Hiding Update Patterns in Secure Outsourced Databases with Differential Privacy[END_REF].

Privacy-preserving dynamic data management has been addressed in a few systems where the focus is on answering queries in a privacy-preserving manner (e.g., [START_REF] Curtmola | Searchable symmetric encryption: improved definitions and efficient constructions[END_REF][START_REF] Hahn | Searchable encryption with secure and efficient updates[END_REF][START_REF] Kamara | SQL on structurally-encrypted databases[END_REF][START_REF] Raluca | CryptDB: processing queries on an encrypted database[END_REF][START_REF] Cetin Sahin | A Differentially Private Index for Range Query Processing in Clouds[END_REF][START_REF] Stefanov | Practical Dynamic Searchable Encryption with Small Leakage[END_REF]), in supporting high insertion rates (e.g., [START_REF] Van Tran | FRESQUE: A Scalable Ingestion Framework for Secure Range Query Processing on Clouds[END_REF]), or in strengthening the privacy model (e.g., [START_REF] Wang | DP-Sync: Hiding Update Patterns in Secure Outsourced Databases with Differential Privacy[END_REF]). For instance, DP-Sync [START_REF] Wang | DP-Sync: Hiding Update Patterns in Secure Outsourced Databases with Differential Privacy[END_REF] addresses the problem of hiding timing database update patterns and guarantees that the entire update history over the outsourced data (in which only a single table schema is supported) is protected using differential privacy techniques. None of these dynamic data management systems, however, support regulated data where data are being updated frequently and updates must satisfy predefined constraints before being incorporated into the data while the privacy of updates, regulations, and/or data needs to be preserved.

Regulated dynamic data have a wide range of applications from single-enterprise settings, where the enterprise data is typically maintained in an outsourced database within an untrusted infrastructure, to multi-enterprise settings, where data is maintained in multiple independent databases owned by a set of mutually distrustful parties. Constraints might be internal constraints defined by the data owners or global regulations defined by external authorities, e.g., some national or governmental institution. For example, in supply chain management, terms of collaborations are internal constraints defined in service level agreements (SLAs) which are agreed upon by all involved participants while in a crowdworking environment, the Fair Labor Standards Act2 (FLSA) is a global regulation that limits the total work hours of a worker per week to not exceed 40 hours.

Verifying incoming updates with respect to such constraints and incorporating the verified updates into data maintained by either untrusted or mutually distrustful infrastructures, on one hand, and guaranteeing the integrity of the stored data, on the other hand, while preserving the privacy of updates, constraints, and data makes the problem challenging. The challenge with respect to privacy is that data managers may not be allowed to [START_REF]AWS. Amazon quantum ledger database (QLDB)[END_REF] view the update, [START_REF]A complete guide to the philosophy of ProvenDB[END_REF] view the data itself and (3) be necessarily aware of the constraints that allow or disallow updates to be incorporated into the databases.

In this paper, we lay out a vision to support privacy-preserving regulated dynamic data. Once data is stored, managing data requires the support of privacy-preserving queries as well as privacy-preserving updates. The underlying infrastructure might consist of a single database owned by a data owner, e.g., an enterprise, or multiple independent databases owned by different distrustful data owners, e.g., different enterprises in a supply chain management. Furthermore, data might be stored remotely on untrusted providers, e.g., cloud servers. While outsourcing data to third parties like the cloud results in higher availability, ease of maintenance, and lower costs, the privacy concerns of data owners need to be addressed. In fact, depending on the application and the underlying infrastructure, the content of the stored data, the content of the updates, and the constraints may be private or public.

In addition to privacy, our vision addresses integrity in order to manage regulated dynamic data. Integrity ensures the checking of updates against constraints and incorporating them into data and enforces the consistency and accuracy of the stored data.

We then present PReVer, a universal framework for managing regulated dynamic data in a privacy-preserving manner. PReVer, on one hand, needs to guarantee (1) the integrity of updates against constraints, (2) the integrity of updates on stored data and (3) the integrity of stored data itself with both single and federated databases and, on the other hand, should be able to preserve [START_REF]AWS. Amazon quantum ledger database (QLDB)[END_REF] the privacy of data, (2) the privacy of updates, or/and (3) the privacy of constraints.

We explore the roadmap leading to systems instantiating the PReVer vision by studying a set of research challenges in two dimensions of privacy and integrity. To guarantee the integrity of updates against constraints and on stored data, PReVer can rely on different privacy-preserving techniques, e.g., fully homomorphic encryption for single database settings [START_REF] Gentry | Fully Homomorphic Encryption Using Ideal Lattices[END_REF], secure multi-party computation and/or token-based mechanisms for federated database settings [START_REF] Javad Amiri | SEPAR: A Privacy-Preserving Blockchainbased System for Regulating Multi-Platform Crowdworking Environments[END_REF], private information retrieval for public data [START_REF] Chor | Private information retrieval[END_REF]. To guarantee the integrity of stored data, the related information should be stored in an immutable and verifiable manner. PReVer relies on append-only ledgers as an immutable verifiable data structure and uses centralized ledger databases [START_REF]AWS. Amazon quantum ledger database (QLDB)[END_REF][START_REF] Yang | LedgerDB: a centralized ledger database for universal audit and verification[END_REF] and permissioned blockchains [7-9, 11, 14, 27, 37, 38, 42, 45, 51, 56, 58] as its infrastructure for single and federated database settings respectively.

PReVer provides database researchers with a framework to explore how to support the scalable efficient execution of private updates on private data sets with constraints. Addressing this challenge requires providing support for the private verifiability of updates on data that is regulated by private or public constraints in a scalable manner as well as a better understanding of information leakage when updates are verified with respect to constraints, where the updates or the constraints may be private or public. This framework can be instantiated using data that is both private or public and where the data is either centralized or sharded across multiple entities in a federated setting. Finally, solutions can be both centralized or distributed, thus providing designers with a range of challenges to explore, especially given the need for practical scalable performance.

The rest of this paper is organized as follows. Section 2 motivates privacy-preserving dynamic data management using several applications. A model for regulated dynamic data is presented in Section 3. Section 4 presents PReVer and explores its research challenges. Section 5 discusses how PReVer can support a specific application, and Section 6 concludes the paper.

MOTIVATION

In this section, we motivate the problem of privacy-preserving dynamic data management using diverse applications. In each case, each of the data, the updates and the constraints may be private or public and data are stored in a single database or multiple databases (i.e., federated setting). Figure 1 presents some of these applications.

Environmental Sustainability

Environmental regulation certification is an important verification process that is critical for successful environmental sustainability. Consider an organization that wants to verify and certify its environmental sustainability efforts with respect to public quantitative sustainability metrics, e.g., ISO 14000 series of standards or LEED (Leadership in Energy and Environmental Design). These claims are certified by a recognized authority that awards Platinum, Gold, or Silver Certificates to companies based on their environmental sustainability statistics or procedures. Usually, since the statistics reflect potential internal organizational operations and hence the organization would like to be certified without revealing sensitive information to the certifying authority, other parties, or the public. Furthermore, these statistics may need to be continuously updated based on changes in the internal processes in these organizations. The data reflecting the organization statistics are stored at the certifying authority as long as the data and the updates are private to the company and are not visible to the certifying authority. However, the regulations are public and widely advertised and are used by the certifying authority to accept or reject specific updates.

As shown in Figure 1(a), if a private update satisfies a public regulation that is issued by some public regulatory, e.g., the International Organization for Standardization, it is executed on a private database. The private database is owned by data owner, however, it is outsourced to a third party, e.g., cloud provider. In this case, the constraints are public, but both the data and the updates need to be private and hidden from the certifying authority. This scenario is typical of many environmental applications, and in general, the certifying authority might also advertise the ranking among a set of competing organizations, based on their environmental sustainability statistic.

In-Person Conference Participation

Consider a conference which proposes both in-person and online participation, however, requires a valid COVID vaccine certification for in-person participation. In this application, the data, the list of in-person attendees, is public, but the update application of the participants demonstrating their vaccination records is private. Needless to say, the constraints regarding admission are public (e.g., testing, vaccination, etc.). As shown in Figure 1(b), For example, when a private update, e.g., a registration record, satisfies a public constraint, e.g., valid COVID vaccine certification requirement, it is executed on public database, e.g., the list of in-person participants.

Multi-Platform Crowdworking

The previous applications all illustrate a single database, where data was stored. Now, we explore multi-site infrastructures. In a multi-platform crowdworking environment, multiple independent competing platforms (e.g, Uber, Lyft, etc) perform private updates (i.e., crowdworking tasks) initiated by participants (i.e., requesters and workers). Consider, for example, a driver who is willing to work for both Lyft and Uber. Whenever the driver performs a task, this is considered an update. Each of Lyft and Uber needs to maintain private records for each driver. However, such updates must satisfy public global regulations, e.g., the total work hours of a worker, who might work for multiple crowdworking platforms, per week may not exceed 40 hours to adhere to Fair Labor Standards Act 3 (FLSA). In this case, private updates need to be executed on multiple private databases stored on platforms that do not trust each other. However, the platforms need to cooperate to verify the public regulations without compromising privacy. Figure 1(c) presents such an application with a federated database system comprising multiple autonomous databases.

Supply Chain Management

Supply chain management is another example of federated database systems where multiple mutually distrustful collaborating enterprises process incoming updates. Lack of trust between different parties is one of the most important problems in supply chain management. Various updates need to be considered, both internal and cross-enterprise, where in contrast to the crossenterprise updates which are visible to multiple enterprises, the internal updates of each enterprise are confidential, e.g., the internal updates of a Manufacturer demonstrate its internal process for producing a product which the Manufacturer might intend to keep as a secret. In such an application the constraints are written as service level agreements agreed upon by all enterprises, hence may be considered public constraints, while depending on the use case data and updates might be public or private. Figure 1(d) shows a supply chain management application with private data, updates, and constraints.

A MODEL FOR PRIVATE REGULATED DYNAMIC DATA

Managing dynamic data in a privacy-preserving manner while guaranteeing the satisfaction of predefined constraints is challenging. In this section, we present a model for privacy-preserving regulated dynamic data management. To preserve the privacy of regulated dynamic data, a threat model also needs to be specified.

Participants

The model consists of four participants roles: data producers, data owners, data managers, and authorities, where a single entity might assume multiple participant roles. Data producers. Data producers produce updates. Data producers might be clients of the system with their own privacy concerns, e.g., requesters in crowdworking environments, or might be public sources of information, e.g., a set of public polar-orbiting satellites that collect data for weather, climate, and environmental monitoring applications. Data owners. Data owners own the data and either maintain data locally or outsource the data to an external third party that manages the data on behalf of the data owner. Data is maintained in either a single database or multiple databases, each owned by a different data owner. Several data owners may co-exist (e.g., federated contexts) and collaborate. Data managers. Data managers store and manage data on behalf of data owners. They are responsible for incorporating updates that are consistent with regulations and constraints into the data as well as responding to queries. We focus on updates as privacypreserving queries have been extensively studied in the literature. If data is stored locally at the data owner, then the data owner also subsumes the role of data manager. However, when data is outsourced to a third party, e.g., a cloud provider, the third party subsumes the role of data management and in general, needs to perform both updates and queries in a privacy-preserving manner. In the case of a single database and to fully demonstrate the privacy challenges, we only focus on outsourced data. Authority. Authorities are mainly in charge of defining constraints. Depending on the type of constraints, i.e., private or public, the authority is either internal or external. An internal authority is equivalent to the data owner who specifies constraints on incoming updates whereas an external authority is an official institution that issues regulations that need to be satisfied by updates before they are incorporated into the database.

Constraints, Updates and Data

A set of constraints specifies the set of allowable database states.

A constraint is essentially a Boolean function computed over the database and an incoming update and expresses a policy for accepting or rejecting incoming updates. Constraints specified by the data owner (e.g., the well-known database constraints) are also called internal constraints. The scope of internal constraints is typically limited to the database(s) of the corresponding data owner: it does not span the databases of multiple data owners. However, constraints may also come from external authorities (e.g., the laws, ethics). We refer to these as regulations below. Unlike internal constraints, a regulation may constrain the databases of multiple data owners (e.g., the money earned monthly by a crowdworker across multiple crowdworking platforms). Given the large body of work for expressing and evaluating database constraints based on data-driven declarative query languages (e.g., relational calculus), these languages are thus a natural choice for expressing regulations. Temporal logic extensions may additionally be relevant for regulations because they often express temporal constraints on sliding time windows, e.g., workers cannot work more than 40 hours a week. An update may involve several participants including at least a data producer and a data manager (e.g., crowdworking application platform). In general, however, an update may originate from the collaboration between several data producers and/or several data managers. For example, consider the multi-platform crowdworking environment. The completion of a crowdworking task is an update that results from the collaboration between two data producers (i.e., a worker and a requester) and at least one data manager (i.e., a crowdworking platform).

An internal constraint is written by an internal authority. As a result, its scope is limited to the database(s) of the corresponding data owner: it does not span the databases of multiple data owners while regulations may constrain the databases of multiple data owners, e.g., the money earned monthly by a crowdworker whatever the crowdworking platform.

Threat Model

Participants such as data managers or clients may adopt adversarial behaviors against the privacy and/or the integrity of the constraints. The threat models considered in PReVer are the usual adversarial models considered in the literature. The choice of a given threat model is not fixed but will depend on each instantiation of the framework, according to the adversarial contexts targeted.

The usual threat models can qualify the kind of adversarial behaviors expected from any kind of participant: honest participants are not expected to adopt adversarial behaviors, honestbut-curious participants strictly follow the algorithm but aim at performing any possible inference (e.g., a dubious outsourced data manager), covert participants deviate from the algorithm only if they are not detected (with a probability above a given threshold), and malicious adversaries deviate arbitrarily from the algorithm. Furthermore, participants may or may not collude. For example in the multi-platform crowdworking instantiation of PReVer, a covert (colluding) adversary model can be considered where participants (i.e., requesters, workers, platforms) may act as covert adversaries and might collude with each other.

Distinguishing the various roles of participants reflects reallife practices. This is well understood by modern data protection laws (see, e.g., GDPR Article 28 about outsourcing, or GDPR Article 32 about the security of processing). The problem of updates is directly related to these laws. Indeed, when data is personal data, it directly falls under the umbrella of the GDPR, and hence, the updates incorporated in PReVer as well. As a result, it is important to understand the leakage of information due to the enforcement of constraints over private data, and hence the need to be protected. However, we note that the case of private constraints over public data is probably more related to intellectual property rather than personal data protection and thus might fall under different legal frameworks.

PREVER FRAMEWORK

PReVer is a universal framework for managing regulated dynamic data in a privacy-preserving manner. PReVer needs to preserve privacy while ensuring integrity in order to guarantee consistent and verifiable execution of updates. PReVer must therefore provide the context for verifying updates against constraints, applying updates to stored data, and maintaining the consistency of stored data while preserving the privacy of updates, constraints and/or data. Figure 2 presents the PReVer framework with two databases. As updates arrive, PReVer needs to provide mechanisms to verify that updates satisfy regulations provided by external authorities or constraints provided by internal authorities. Once verified, the update needs to be applied to the databases. Finally, PReVer needs to provide techniques that guarantee that databases have not been corrupted.

In general, PReVer needs to deal with several challenges. First, while most privacy-preserving techniques focus on the querying goal, PReVer needs to verify updates that results in additional challenges, e.g., disclosing update patterns [START_REF] Wang | DP-Sync: Hiding Update Patterns in Secure Outsourced Databases with Differential Privacy[END_REF]. Second, most privacy-preserving techniques do not scale and are computationally expensive. Third, constraints and regulations have not been supported in any of these techniques. They require the untrusted data manager(s) to perform computations on the encrypted database and not only to retrieve tuples.

In this section, we explore the roadmap leading to systems instantiating the PReVer vision. We explore a set of challenges that PReVer needs to address in order to guarantee the privacypreserving integrity of updates against constraints and on stored data as well as ensuring the privacy-preserving integrity of stored data. For each of these challenges, we highlight the limitations of current privacy-preserving mechanisms. Single private database. PReVer needs to address the setting where an untrusted data manager maintains the data, e.g., atmosphere monitoring databases application or environmental sustainability application.

Research Challenge 1. Enable an untrusted data manager to verify updates against constraints and execute updates on private data in a privacy-preserving manner.

Traditionally, when a query is private, privacy-preserving querying techniques hide it by encrypting it or by generating trapdoors that enable the data manager to perform the search without leaking the query. In PReVer, a constraint can be private, but hiding it requires to go beyond hiding the search values in order to protect the complete Boolean function that implements the constraint. Moreover, an update must eventually be executed on data or discarded depending on the Boolean output of the constraint. Performing or discarding updates must be done without jeopardizing privacy guarantees.

To address Research Challenge 1, PReVer can be built on existing privacy-preserving querying techniques such as fully homomorphic encryption [START_REF] Boneh | Private Database Queries Using Somewhat Homomorphic Encryption[END_REF] (thus providing software protected computation) -or more generally functional encryption [START_REF] Boneh | Functional encryption: a new vision for public-key cryptography[END_REF] and zero-knowledge succinct non-interactive arguments of knowledge [START_REF] Fiore | Boosting Verifiable Computation on Encrypted Data[END_REF] to address the integrity of constraints (basically requiring the untrusted manager to provide verifiable proofs that they actually perform the correct actions they claim.). Such techniques, however, have considerable overhead [START_REF] Zhang | Spitz: A Verifiable Database System[END_REF][START_REF] Zhang | vSQL: Verifying Arbitrary SQL Queries over Dynamic Outsourced Databases[END_REF][START_REF] Zhou | VeriDB: An SGX-based Verifiable Database[END_REF]. Alternatively, PR-eVer can rely on differentially private indexing, i.e., partial disclosures [START_REF] Cetin Sahin | A Differentially Private Index for Range Query Processing in Clouds[END_REF][START_REF] Van Tran | FRESQUE: A Scalable Ingestion Framework for Secure Range Query Processing on Clouds[END_REF]. However, naive uses of differential privacy lead to rapidly exhausting the limited privacy budget, especially when updates come at a high rate. This results either in an impossibility to support additional updates or in an uncontrolled increase of the noise magnitude. To improve the performance of updates, secure hardware, i.e., hardware protected computation [START_REF] Anciaux | Personal Data Management Systems: The security and functionality standpoint[END_REF][START_REF] Arasu | Transaction processing on confidential data using cipherbase[END_REF][START_REF] Bajaj | TrustedDB: A Trusted Hardware-Based Database with Privacy and Data Confidentiality[END_REF][START_REF] Priebe | EnclaveDB: A Secure Database Using SGX[END_REF][START_REF] Sun | Building Enclave-Native Storage Engines for Practical Encrypted Databases[END_REF] can be used. However, secure hardware has scalability issues. Multiple private databases. Thus far, we have focused on a single database, however, as our application examples clearly demonstrate, e.g., multi-platform crowdworking or supply chain management, many applications require a federation of databases. These databases need to collectively verify constraints in a distributed manner and apply updates to individual databases without violating the distributed constraints.

Federated contexts require distributed solutions for allowing multiple data managers, trusted or not, to verify updates against constraints and to execute them on stored data in a collaborative manner while protecting the data they host, and, if required, the constraints and the updates.

Research Challenge 2. Enable a set of trusted and untrusted federated data managers to verify distributed constraints over distributed private data and to perform updates conditionally, all this with sound privacy and integrity guarantees.

Traditionally, such problems have been solved using centralized or distributed approaches. In a centralized approach, a tokenbased mechanism can be used to ensure the verifiability of distributed constraints over distributed private data. A token-based system, e.g., e-cash, implements constraints and regulations by managing budgets per participant called tokens. Tokens are singleuse cryptographic tokens (i.e., a nonce signed by a trusted authority stored in a public database once spent) that are generated periodically by an external authority and distributed to corresponding participants. Alternatively, secure multi-party computation [START_REF] Chaum | Multiparty computations ensuring privacy of each party's input and correctness of the result[END_REF] can be used as a decentralized approach. Using secure multi-party computation, different data managers could collaborative verify updates against constraints and apply it to their databases (see, e.g., [START_REF] Alonso | Partitioned data objects in distributed databases[END_REF][START_REF] Barbard | The Demarcation Protocol: A technique for maintaining linear arithmetic constraints in distributed database systems[END_REF] in un-protected contexts).

To address Research Challenge 2, PReVer can be built on a centralized token-based mechanism and decentralized secure multi-party computation. However, token-based mechanisms can only address simple COUNT-aggregate queries and it is unclear how they can be generalized to support other kinds of constraints. Traditional secure multi-party computations, on the other hand, either do not handle updates or usually assume each of the distributed parties is trusted (just that they do not trust each other). However, in the context of PReVer when some data managers are untrusted, the challenge is especially hard because these data managers have no access to raw data and consequently, their computation abilities are strongly reduced. Applying updates satisfying the constraints to each federated data manager rises additional challenges similar to those discussed earlier. Furthermore, in a dynamic setting, PReVer can benefit from the efficient incremental techniques. In general constraint enforcement in a privacy-preserving manner has not been sufficiently explored and seems to be an open area for future research. Public databases. Finally, PReVer needs to address applications, e.g., in-person conference participation during the COVID pandemic, where the data itself is public, but the constraints and updates might be private.

Research Challenge 3. Enable a data manager to verify updates against constraints over public data and execute the updates with sound privacy guarantees on the updates.

Private Information Retrieval (PIR) techniques [START_REF] Chor | Private information retrieval[END_REF][START_REF] Aguilar Melchor | XPIR : Private Information Retrieval for Everyone[END_REF] have been traditionally used to address privacy-preserving queries when data is public. PIR allows users to retrieve items from a public database by specifying an index without revealing the items retrieved.

To address Research Challenge 3, two challenges need to be addressed. First, PIR techniques have been restricted to retrieving a single item in a privacy-preserving manner. This needs to be extended with computational capabilities to verify complex (SQL-like) constraints irrespective of whether they are private or public. If the constraints are private, there is an additional need to consider the non-negligible leak about private constraints resulting from applying updates to public data. Second, while PIR techniques are designed primarily to support private retrieval of information, in PReVer, these techniques need to be extended to support updates. Recently, there have been many attempts to improve the performance of PIR [START_REF] Ahmad | Addra: Metadata-private voice communication over fully untrusted infrastructure[END_REF][START_REF] Angel | PIR with compressed queries and amortized query processing[END_REF][START_REF] Aguilar Melchor | XPIR: Private information retrieval for everyone[END_REF], however, more research needs to be conducted to efficiently support updates.

Integrity of stored data. Finally, PReVer needs to guarantee the integrity of stored data in both single and federated databases. The main challenge is to enable any of the participants to verify the integrity of stored data in a privacy-preserving manner.

Research Challenge 4. Enable any participant to verify the integrity of stored data with sound privacy guarantees.

In PReVer, data needs to be stored in an immutable and verifiable manner. Immutability prevents any malicious participants from altering data and verifiability enables all (authorized) participants to check the state of the system. Append-only ledgers provide the immutability and verifiability features required by PReVer. Append-only ledgers use authenticated data structures such as Merkle trees [START_REF] Merkle | A Digital Signature Based on a Conventional Encryption Function[END_REF] to ensure that data is tamper-resistant when the underlying infrastructure is untrusted. When there is a single database maintained by a single data manager, the centralized ledger technology can be used as the infrastructure of PReVer where a ledger database provides tamper-evidence and verification features in a centralized manner. Alibaba LedgerDB [START_REF] Yang | LedgerDB: a centralized ledger database for universal audit and verification[END_REF], Amazon QLDB [START_REF]AWS. Amazon quantum ledger database (QLDB)[END_REF], and ProvenDB [START_REF]A complete guide to the philosophy of ProvenDB[END_REF] are some of the existing centralized ledger databases. Verifiable database techniques [START_REF] Benabbas | Verifiable Delegation of Computation over Large Datasets[END_REF][START_REF] Chen | Publicly Verifiable Databases with All Efficient Updating Operations[END_REF][START_REF] Fiore | Efficiently Verifiable Computation on Encrypted Data[END_REF] have also been used to verify the integrity of stored data. Such techniques, however, are more specific to database queries and their ability to support computation beyond the search is unclear.

To address Research Challenge 4, these techniques need to be extended to the distributed setting. Since an update can be processed on all or a subset of databases, processing updating requires establishing consensus among all involved data managers. Moreover, the data managers might not trust each other. To address these challenges, permissioned blockchain systems, e.g., Hyperledger Fabric [START_REF] Androulaki | Hyperledger Fabric: a distributed operating system for permissioned blockchains[END_REF], can be used as the infrastructure of PReVer. While Fabric uses private data collections [3] to ensure confidentiality, its computational overhead is significant and results in reduced throughput. To address the computational overhead of Fabric, PReVer can leverage some of the techniques developed in Qanaat [START_REF] Javad Amiri | Qanaat: A Scalable Multi-Enterprise Permissioned Blockchain System with Confidentiality Guarantees[END_REF]. In particular, to support confidentiality, Qanaat enables every subset of data managers to form a confidential collaboration private from other enterprises thus enabling them to execute updates. Qanaat further provides scalability by partitioning data into data shards. These techniques can be leveraged by PReVer in order to ensure the integrity of stored data in a privacy-preserving manner.

AN APPLICATION OF PREVER

The goal of PReVer is to present a general framework for managing regulated dynamic data in a privacy-preserving manner. In general, choosing the right set of techniques depends on three main criteria: (1) data is private or public, (2) the database is single or federated, and (3) the instatiation is centralized or decentralized. In this section, we discuss how PReVer can be used to support multi-platform crowdworking applications. Our goal is to provide a specific instance of PReVer and to illustrate how a particular system, Separ [START_REF] Javad Amiri | SEPAR: A Privacy-Preserving Blockchainbased System for Regulating Multi-Platform Crowdworking Environments[END_REF], was able to solve several of the challenges discussed in Section 4. In Separ's instantiation of PRe-Ver, the data and the updates are private while the constraints are public, the database is federated, and a centralized tokenbased approach is chosen. Furthermore, we highlight several of the shortcomings of Separ, thus demonstrating the need for future research to address general solutions for privacy-preserving crowdworking applications.

Separ is a multi-platform crowdworking system, where workers may need to work for or avail from the services of multiple crowdworking platforms, e.g., a driver may work through both Uber and Lift. Separ needs to enforce public global regulations (e.g., future of work labor laws like a limit on the number of hours worked), in a privacy-preserving manner, on a set of distributed independent platforms that are mutually distrustful of each other. Workers are the data producers and data owners in PReVer, while the multiple platforms are the data managers. Separ uses a trusted third party to act as the authority that expresses public regulations. Platforms do not trust each other and workers do not want to share their personal data (e.g., tasks completed, exact number of hours worked) from one platform to another. However, the global regulatory constraints need to be enforced in a privacy-preserving manner. As a result, the constraints are the (public) upper-bound regulations 4 , the data is the (private) task completion database (Separ does not need to instantiate it but keeps it virtual), and the updates are (private) information about the completion of a task (e.g., task completed, time spent, requester, platform).

Separ uses a centralised trusted authority to enforce regulations using single-use, pseudonymous tokens, which ensure that mutually distrustful platforms can cooperate to enforce the distributed constraints for the conditional execution of updates (Research Challenge 2). It relies on the permissioned blockchain system SharPer [START_REF] Javad Amiri | SharPer: Sharding Permissioned Blockchains Over Network Clusters[END_REF] to guarantee integrity of the global system state (i.e., the tokens spent -Research Challenge 4). The global system state is shared among the mutually distrustful crowdworking platforms using distributed consensus protocols over the blockchain ledgers (for immutability and verifiability).

Separ represents a particular instantiation of PReVer. A general multi-platform crowdworking application would need to address several of Separ's limitations. We discuss some of these here, and leave the solutions for future work. Separ requires a centralized trusted third party authority to issue tokens. This is a serious shortcoming, as a general distributed approach should be used to enforce distributed constraints on updates in a privacy preserving manner. Furthermore, Separ focuses on lower and upper bound constraints. Future systems should support general distributed constraints, e.g., any SQL expressed constraints, including GROUP BY, JOIN and aggregate expressions, which might require the use of secure multi-party computations. Furthermore, the adversarial model in Separ assumes that participants do not collude, which is not realistic in many adversarial settings. A general multi-platform solution should assume collusion among participants and provide efficient protocols in such diverse settings. The PReVer framework also highlights some shortcoming in the Separ approach, namely restricting regulations to public constraints as it is quite realistic to assume constraints among a subset of the platforms. Another shortcoming highlighted by PReVer can be used to support many other applications. For instance, to support supply chain management applications (Figure 1(d)), PReVer can use permissioned blockchains to guarantee the integrity of stored data (Research Challenges 4). To address the integrity requirement in the execution of smart contracts, PReVer can rely on zero-knowledge proofs when the smart contract depends on the private data of a single database: the data manager who knows the secret can run the smart contract on its own, and then prove to everyone else that it did so correctly. However, zero-Knowledge Proofs are not sufficient in settings where the smart contract depends on the secret information of multiple data managers [START_REF] Benhamouda | Supporting private data on hyperledger fabric with secure multiparty computation[END_REF]. To address Research Challenge 2, using secure-MPC protocols to support private data on Hyperledger Fabric has been proposed [START_REF] Benhamouda | Supporting private data on hyperledger fabric with secure multiparty computation[END_REF] where the execution of the secure-MPC protocol is integrated as part of the smart contract. PReVer can also rely on RIP to address Research Challenge 3 in supply chain management when data is public. 4 Separ also supports lower-bound regulations.

DISCUSSION AND CONCLUSIONS

In this paper, we lay out a vision to design PReVer, a universal framework for managing regulated dynamic data in a privacypreserving manner. Data in PReVer is maintained by either untrusted or mutually distrustful infrastructures and updates need to be verified and incorporated into databases based on predefined constraints.

Any implementation of the PReVer framework needs to address several critical research questions that we pose to the database community as challenges that need to be addressed to ensure the successful management of regulated privacy preserving dynamic data management systems. In a nutshell database and systems researchers need to clearly demonstrate how to support scalable efficient consistent and verifiable execution of updates on data with constraints while preserving privacy.

Designing such systems requires solving multiple challenges:

• Private verification. The efficient verification of an update with respect to a given generally formulated constraint where the update and the constraint or both might have privacy constraints with respect to the data manager. • Private updates. The efficient execution of an update on data where the update and the data or both might have privacy constraints with respect to the data manager. • Scalable solutions. These solutions need to scale with respect to the frequency of updates as well as the size of the data.

PReVer thus requires a better understanding of information leakage due to the enforcement of constraints on updates. Furthermore, these challenges need to be addressed in multiple contexts:

• Private and public databases. The data is private or public with a stream of updates and data constraints that may be private. • Centralized and federated decentralized databases. The data can be stored in one centralized location or may be sharded across multiple sites, with different organizational supervision.

PReVer provides a framework that would allow database, cryptography and distributed systems researchers to explore implementing parts of this general vision. In particular, the framework facilitates the ability for researchers to restrict their practical implementation to the most appealing context they are interested in, e.g., centralized private data, federated public settings, etc.

PReVer presents a framework based on four main components: data owners, data providers, data managers, and regulatory authorities. These abstractly capture the essential and relevant components needed for a focused study of private dynamic data management and would allow researchers to identify the context they wish to explore and hence focus on the efficiency and scalability of their solutions. It is interesting to note that in spite of the variety of contexts, from a storage point of view, the ledger model seems quite versatile for so many varied contexts.

Ideally, and to ensure solutions are actionable, comparisons should be performed with respect to non-private solutions using standardized database benchmarks like TPC and YCSB. Furthermore the distributed solutions should be compared in terms of throughput and latency with standard distributed fault-tolerant protocols, e.g., Paxos [START_REF] Lamport | Paxos made simple[END_REF] and PBFT [START_REF] Castro | Practical Byzantine fault tolerance[END_REF].

Figure 1 :

 1 Figure 1: Some possible applications of privacy-preserving dynamic data management

Figure 2 :

 2 Figure 2: PReVer framework consisting of two databases. (0): Authorities define constraints and regulations, (1): The data producer sends an update, (2): The update is verified with respect to regulations and constraints, and (3): The update is incorporated into data.

We overload below the term privacy for referring to both the privacy of personal data (our main focus) and to the confidentiality of data that is non-personal.

https://www.dol.gov/agencies/whd/flsa Vision Paper Series ISSN: 2367-2005

https://www.dol.gov/agencies/whd/flsa

ACKNOWLEDGMENTS

This work is funded by NSF grants CNS-1703560, CNS-1815733, and CNS-2104882 and by the ANR grant ANR-16-CE23-0004.


Franck Cassez
email: franck.cassez@cnrs.irccyn.fr

Stavros Tripakis
email: tripakis@cadence.com

Karine Altisen

Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis * (Extended Abstract)

We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists of synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider static as well as dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe.

Introduction

Monitoring, Testing, Fault Diagnosis and Control. Many problems concerning the monitoring, testing, fault diagnosis and control of discrete event systems (DES) can be formalized by using finite automata over a set of observable events Σ, plus a set of unobservable events [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF][START_REF] Tsitsiklis | On the control of discrete event dynamical systems[END_REF]. The invisible actions can often be represented by a single unobservable event ε. Given a finite automaton over Σ ∪ {ε} which is a model of a plant (to be monitored, tested, diagnosed or controlled) and an objective (good behaviours, what to test for, faulty behaviours, control objective) we want to check if a monitor/tester/diagnoser/controller exists that achieves the objective, and if possible to synthesize one automatically.

The usual assumption in this setting is that the set of observable events is fixed (and this in turn determines the set of unobservable events as well). Observing an event usually requires some detection mechanism, i.e. , a sensor of some sort. Which sensors to use, how many of them, and where to place them are some of the design questions that are often difficult to answer, especially without knowing what these sensors are to be used for.

In this paper we study problems of sensor minimization. These problems are interesting since observing an event can be costly in terms of time or energy: computation time must be spent to read and process the information provided by the sensor, and power is required to operate the sensor (as well as to perform the computations). It is then essential that the sensors used really provide useful information. It is also important for the computer to discard any information given by a sensor that is not really needed. In the case of a fixed set of observable events, it is not the case that all sensors always provide useful information and sometimes energy (sensor operation and computer treatment) is spent for nothing. For example, to diagnose a fault in the system described by the automaton B, Figure 3, an observer only has to watch event a, and when a has occurred, to watch event b: if the sequence a.b occurs, for sure a fault has occurred and the observer can raise an alarm. It is then not useful to switch on sensor b before an a has occurred.

Sensor Minimization and Fault Diagnosis. We focus our attention on sensor minimization, without looking at problems related to sensor placement, choosing between different types of sensors, and so on. We also focus on a particular observation problem, that of fault diagnosis. We believe, however, that the results we obtain are applicable to other contexts as well.

Fault diagnosis consists in observing a plant and detecting whether a fault has occurred or not. We follow the discrete-event system (DES) setting of [START_REF] Sampath | Teneketzis. Diagnosability of discrete event systems[END_REF] where the behavior of the plant is known and a model of it is available as a finite-state automaton over Σ ∪ {ε, f } where Σ is the set of observable events, ε represents the unobservable events, and f is a special unobservable event that corresponds to the faults. Checking diagnosability (whether a fault can be detected) for a given plant and a fixed set of observable events can be done in polynomial time [START_REF] Sampath | Teneketzis. Diagnosability of discrete event systems[END_REF][START_REF] Yoo | On the computational complexity of some problems arising in partially-observed discrete event systems[END_REF][START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF]. (Notice that synthesizing a diagnoser involves determinization in general, thus cannot be done in polynomial time.)

We examine sensor optimization problems with both static and dynamic observers. A static observer always observes the same set of events, whereas a dynamic observer can modify the set of events it wishes to observe during the course of the plant execution (this could be implemented by switching sensors on and off in order to save energy, for example).

In the static observer case, we consider both the standard setting of observable/unobservable events as well as the setting where the observer is defined as a mask which allows some events to be observable but not distinguishable (e.g., see [START_REF] Cieslak | Supervisory control of discrete-event processes with partial observations[END_REF]). Our first contribution is to show that the problems of minimizing the number of observable events (or distinct observable outcomes in case of the mask) are NP-complete. Membership in NP can be easily derived by reducing these problems to the standard diagnosability problem, once a candidate minimal solution is chosen non-deterministically. NP-hardness can be shown using reductions of well-known NP-hard problems, namely, clique and coloring problems in graphs.

In the dynamic observer case, we assume that an observer can decide after each new observation the set of events it is going to watch. As a second contribution, we provide a definition of the dynamic observer synthesis problem and then show that computing a dynamic observer for a given plant, can be reduced to a game problem.

Related work.

NP-hardness of finding minimum-cardinality sets of observable events so that diagnosability holds under the standard, projection-based setting has been previously reported in [START_REF] Yoo | On the computational complexity of some problems arising in partially-observed discrete event systems[END_REF]. Our result of section 3 can be viewed as an alternative shorter proof of this result. Masks have not been considered in [START_REF] Yoo | On the computational complexity of some problems arising in partially-observed discrete event systems[END_REF]. As we show in section 4, a reduction from the mask version of the problem to the standard version is not straightforward. Thus the result in section 4 is useful and new.

The complexity of finding "optimal" observation masks, i.e. a set that cannot be reduced, has been considered in [START_REF] Jiang | Optimal sensor selection for discrete event systems with partial observation[END_REF] where it was shown that the problem is NP-hard for general properties. [START_REF] Jiang | Optimal sensor selection for discrete event systems with partial observation[END_REF] also shows that finding optimal observation masks is polynomial for "mask-monotonic" properties where increasing the set of observable (or distinguishable) events preserves the property in question. Diagnosability is a mask-monotonic property. Notice that optimal observation masks are not the same as minimum-cardinality masks that we consider in our work.

In [START_REF] Debouk | On an optimization problem in sensor selection[END_REF], the authors investigate the problem of computing a minimal-cost strategy that allows to find a subset of the set of observable events s.t. the system is diagnosable. It is assumed that each such subset has a known associated cost, as well as a known a-priori probability for achieving diagnosability.

To our knowledge, the problems of synthesizing dynamic observers for diagnosability, studied in Section 5, have not been addressed previously in the literature. The material of this paper is taken from [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] which contains a follow-up part of the present paper that studies the problem of optimal-cost dynamic observers synthesis [START_REF] Cassez | Synthesis of optimal-cost dynamic diagnosers for fault diagnosis of discrete-event systems[END_REF].

Organisation of the paper. In Section 2 we fix notation and introduce finite automata with faults to model DES. In Section 3 we show NP-completeness of the sensor minimization problem for the standard projection-based observation setting. In Section 4 we show NP-completeness of the sensor minimization problem for the mask-based setting. In Section 5 we introduce and study dynamic observers. We define dynamic observers and show that the most permissive dynamic observer can be computed as the strategy in a safety 2-player game.

A full version of the paper containing the omitted proofs is available from the web page of the authors.

Preliminaries

Words and Languages

Let Σ be a finite alphabet and Σ ε = Σ ∪ {ε}. Σ * is the set of finite words over Σ and contains ε which is also the empty word. A language L is any subset of Σ * . Σ + = Σ * \ {ε}. Given two words ρ, ρ ′ we denote ρ.ρ ′ the concatenation of ρ and ρ ′ (which is defined in the usual way). |ρ| stands for the length of the word ρ and |ρ| λ with λ ∈ Σ stands for the number of occurrences of λ in ρ. Given Σ 1 ⊆ Σ, we define the projection π /Σ1 : Σ * → Σ * 1 by: π /Σ1 (ε) = ε and for a ∈ Σ, ρ ∈ Σ * , π /Σ1 (a.ρ) = a.π /Σ1 (ρ) if a ∈ Σ 1 and π /Σ1 (ρ) otherwise.

Finite Automata

Let f ∈ Σ ε be a fresh letter that corresponds to the fault action. An automaton A is a tuple 1

(Q, q 0 , Σ ε,f , →) with Q a set of states, q 0 ∈ Q is the initial state, →⊆ Q × Σ ε,f × Q is the transition relation. If Q is finite, A is a finite automa- ton. We write q λ -→ q ′ if (q, λ, q ′ ) ∈ → . For q ∈ Q, en(q) is the set of actions enabled at q. A run ρ from state s in A is a sequence of transitions s 0 λ1 --→ s 1 λ2 --→ s 2 • • • s n-1 λn --→ s n s.t. λ i ∈ Σ ε,
f and s 0 = s. We let tgt(ρ) = s n . The set of runs from s in A is denoted Runs(s, A) and we define Runs(A) = Runs(q 0 , A). The trace of the run ρ, denoted tr(ρ), is the word obtained by concatenating the symbols λ i appearing in ρ, for those λ i different from ε. Given a set R ⊆ Runs(A), Tr(R) = {tr(ρ) for ρ ∈ R} is the set of traces of the runs in R. A run ρ is k-faulty if there is some 1 ≤ i ≤ n s.t. λ i = f and ni ≥ k. Faulty ≥k (A) is the set of k-faulty runs of A. A run is faulty if it is k-faulty for some k ∈ N and Faulty(A) denotes the set of faulty runs. It follows that Faulty ≥k+1 (A) ⊆ Faulty ≥k (A) ⊆ • • • ⊆ Faulty ≥0 (A) = Faulty(A). Finally NonFaulty(A) = Runs(A) \ Faulty(A) is the set on nonfaulty runs of A. We let Faulty tr ≥k (A) = Tr(Faulty ≥k (A)) and NonFaulty tr (A) = Tr(NonFaulty(A)) be the sets of traces of faulty and non-faulty runs.

A word w is accepted by A if w = tr(ρ) for some ρ ∈ Runs(A). The language L(A) of A is the set of words accepted by A. We assume that each faulty run of A of length n can be extended into a run of length n + 1. This is required for technical reasons (in order to guarantee that the set of faulty runs where sufficient time has elapsed after the fault is well-defined) and can be achieved by adding ε loop transitions to each deadlock state of A. Notice that this transformation does not change the observations produced by the plant, thus, any observer synthesized for the transformed plant also applies to the original one.

Finally Product of Automata without ε-transitions are defined in the usual way: they synchronize on common letters.

Sensor Minimization with Static Observers

In this section we address the sensor minimization problem for static observers. We point out that the result in this section was already obtained in [START_REF] Yoo | On the computational complexity of some problems arising in partially-observed discrete event systems[END_REF] and we only give here an alternative shorter proof. We are given a finite automaton A = (Q, q 0 , Σ ε,f , →). The maximal set of observable events is Σ (ε is not observable). We want to decide whether there is a subset Σ o Σ such that the faults can be detected by observing only events in Σ o . Moreover, we would like to find an "optimal" such Σ o .

A diagnoser is a device that observes the plant and raises an "alarm" whenever it detects a fault. We allow the diagnoser to raise an alarm not necessarily immediately after the fault occurs, but possibly some time later, as long as this time is bounded by some k ∈ N. We model time by counting the "moves" the plant makes (including observable and unobservable ones). If the system generates a word ρ but only a subset Σ o ⊆ Σ is observable, the diagnoser can only see π /Σo (ρ).

Definition 1 ((Σ

o , k)-Diagnoser) Let A be a finite auto- maton over Σ ε,f , k ∈ N, Σ o ⊆ Σ. A mapping D : Σ * o → {0, 1} is a (Σ o , k)-diagnoser for A if (i) for each ρ ∈ NonFaulty(A), D(π /Σo (tr(ρ))) = 0, and (ii) for each ρ ∈ Faulty ≥k (A), D(π /Σo (tr(ρ))) = 1. A is (Σ o , k)-diagnosable if there is a (Σ o , k)-diagnoser for A. A is Σ o -diagnosable if there is some k ∈ N s.t. A is (Σ o , k)-diagnosable.
Example 1 Let A be the automaton shown on Figure 1. The run f is in Faulty ≥0 (A), the run f.a is in Faulty ≥1 (A) and a.ε 2 is in NonFaulty(A).

• • • • • ε ε f a b a b

Figure 1. The automaton A

A is neither {a}-diagnosable, nor {b}-diagnosable. This is because, for any k, the faulty run f.a.b.ε k gives the same observation as the non-faulty run a.ε k (in case a is the observable event) or the non-faulty run b.ε k (in case b is the observable event). Consequently, the diagnoser cannot distinguish between the two no matter how long it waits. If both a and b are observable, however, then we can define:

D(a.b.ρ) = 1 for any ρ ∈ {a, b} * and D(ρ) = 0 otherwise. D is a ({a, b}, 2)-diagnoser for A.
For given A and Σ o it is known how to check diagnosability and build a diagnoser (e.g., see [START_REF] Sampath | Teneketzis. Diagnosability of discrete event systems[END_REF]). Checking whether

A is Σ o -diagnosable can be done in polynomial time in the size of A, more precisely in O(|A| 2 ). Computing the minimum k s.t. A is (Σ o , k)-diagnosable can be done in O(|A| 3 ).
Moreover in case A is Σ o -diagnosable, there is a diagnoser D that can be represented by a finite automaton. Computing this finite automaton is in O(2 |A| ). Algorithms for solving these problems are given in appendix A in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] and use the

fact that A is (Σ o , k)-diagnosable iff π /Σo (Faulty tr ≥k (A)) ∩ π /Σo (NonFaulty tr (A)) = ∅ (1)
or in other words, there is no pair of runs (ρ 1 , ρ 2 ) with ρ 1 ∈ Faulty ≥k (A), ρ 2 ∈ NonFaulty(A) s.t. ρ 1 and ρ 2 give the same observations on Σ o . In this section we address the problem of finding a set of observable events Σ o that allows faults to be detected. We would like to detect faults using as few observable events as possible.

Problem 1 (Minimum Number of Observable Events)

INPUT: A, n ∈ N s.t. n ≤ |Σ|. PROBLEM: (A) Is there any Σ o ⊆ Σ with |Σ o | = n, such that A is Σ o -diagnosable? (B
) If the answer to (A) is "yes", find the minimum n 0 such that there exists

Σ o ⊆ Σ with |Σ o | = n 0 and A is Σ o -diagnosable.
If we know how to solve Problem 1(A) efficiently then we can also solve Problem 1(B) efficiently: we perform a binary search over n between 0 and |Σ|, and solve Problem 1(A) for each such n, until we find the minimum n 0 for which Problem 1(A) gives a positive answer. 2 Unfortunately, Problem 1(A) is a combinatorial problem, exponential in |Σ|, as we show next.

Theorem 1 Problem 1(A) is NP-complete.

Proof: (Sketch) Membership in NP is easy: guess a solution Σ o and check Σ o -diagnosability (can be done in polynomial time). The proof of NP-hardness is a reduction of the nclique problem to Problem 1(A). Details can be found in the extended version of the paper.

Sensor Minimization with Masks

So far we have assumed that observable events are also distinguishable. However, there are cases where two events a and b are observable but not distinguishable, that is, the diagnoser knows that a or b occurred, but not which of the two. This is not the same as considering a and b to be unobservable, since in that case the diagnoser would not be able to detect occurrence of a or b. Distinguishability of events is captured by the notion of a mask.

Definition 2 (Mask

) A mask (M, n) over Σ is a total, sur- jective function M : Σ → {1, • • • , n} ∪ {ε}. M induces a morphism M * : Σ * → {1, • • • , n} * . For example, if Σ = {a,

Definition 3 ((

M, n), k)-diagnoser) Let (M, n) be a mask over Σ. A mapping D : {1, • • • , n} * → {0, 1} is a ((M, n), k)-diagnoser for A if (i) for each ρ ∈ NonFaulty(A), D(M * (π /Σ (tr(ρ)))) = 0 and (ii) for each ρ ∈ Faulty ≥k (A), D(M * (π /Σ (tr(ρ)))) = 1. A is ((M, n), k)-diagnosable if there is a ((M, n), k)- diagnoser for A. A is (M, n)-diagnosable if there is some k such that A is ((M, n), k)-diagnosable.
Given A and a mask (M, n), checking whether A is (M, n)-diagnosable can be done in polynomial time. In fact it can be reduced to checking Σ o -diagnosability of a modified automaton A M , with

Σ o = {1, ..., n}. A M is obtained from A by renaming the actions a ∈ Σ by M (a). It can be seen that A is ((M, n)-diagnosable iff A M is {1, • • • , n}- diagnosable. Notice that A is ((M, n), k)-diagnosable iff M * (π /Σ (Faulty tr ≥k (A))) ∩ M * (π /Σ (NonFaulty tr (A))) = ∅.
As in the previous section, we are mostly interested in minimizing the observability requirements while maintaining diagnosability. In the context of diagnosis with masks, this means minimizing the number n of distinct outputs of the mask M . We thus define the following problem:

Problem 2 (Minimum Mask) INPUT: A, n ∈ N s.t. n ≤ |Σ|. PROBLEM: (A) Is there any mask (M, n) such that A is (M, n)- diagnosable?
(B) If the answer to (A) is "yes", find the minimum n 0 such that there is a mask

(M, n 0 ) such that A is (M, n 0 )- diagnosable.
As with Problem 1, if we know how to solve Problem 2(A) efficiently we also know how to solve Problem 2(B) efficiently: again, a binary search on n suffices.

We will prove that Problem 2 is NP-complete. One might think that this result follows easily from Theorem 1. However, this is not the case. Obviously, a solution to Problem 1 provides a solution to Problem 2: assume there exists Then A is ((M, 1), 2)-diagnosable because we can build a diagnoser D defined by: D(ε) = 0, D(1) = 0, D(1 2 .ρ) = 1 for any ρ ∈ 1 * . However, as we said before, there is no strict subset of {a, b} that allows A to be diagnosed.

Σ o such that A is (Σ o , k)-diagnosable and Σ o = {a 1 , ..., a n }; define a mask M : Σ → {1, • • • , n} such that M (a i ) = i and for any a ∈ Σ \ Σ o , M (a) = ε. Then, A is ((M, n), k)-diagnosable.

Theorem 2 Problem 2 is NP-complete.

Proof: Membership in NP is again justified by the fact that checking whether a guessed mask works can be done in polynomial time (it suffices to rename the events of the system according to M and apply the algorithm of appendix A in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF]). We show NP-hardness using a reduction of the ncoloring problem. The n-coloring problem asks the following: given an undirected graph G = (V, E), is it possible to color the vertices with colors in {1, 2, • • • , n} so that no two adjacent vertices have the same color? Let G = (V, E) be an undirected graph. Let E = {e 1 , e 2 , • • • , e j } be the set of edges with e i = (u i , v i ). We let Σ = V and define the automaton A G as pictured in Figure 2. The initial state of

A G is q 0 . We claim that G is n-colorizable iff A G is (M, n)-diagnosable. Widget for e 2 q 0 • • • • • • • • • • • • • • • • • • • u 1 f v 1 u 2 f v 2 u j f v j v 1 ε u 1 v 2 ε u 2 v j ε u j • • • ε ε ε ε Figure 2. Automaton A G for n-colorizability If part. Assume A G is (M, n)-diagnosable for n ≥ 0.
We first show that for all i = 1, ..., j, M

(u i ) = ε, M (v i ) = ε and M (u i ) = M (v i ).
For any k, we can define the runs ρ

= v 1 .ε.u 1 .v 2 .ε.u 2 • • • u i .f.v i .ε k and ρ ′ = v 1 .ε.u 1 .v 2 .ε.u 2 • • • v i .ε.u i . If either M (u i ) = ε or M (v i ) = ε or M (u i ) = M (v i ) holds, then we have M * (π /Σ (tr(ρ))) = M * (π /Σ (tr(ρ ′ ))
). This way for any k, there is a faulty run with more than k events after the fault, and a non-faulty run which gives the same observation through the mask. Hence A cannot be ((M, n), k)diagnosable for any k and thus A is not (M, n)-diagnosable which contradicts diagnosability of A. Note that the above implies in particular that n ≥ 1. We can now prove that G is n-colorizable. Let C be the color mapping defined by C(v) = M (v). We need to prove that C(u i ) = C(v i ) for any (u i , v i ) ∈ E. This holds by construction of A G and the fact that M (u i ) = M (v i ) as shown above.

Only if part. Assume G is n-colorizable. There exists a color mapping

C : V → {1, 2, • • • , n} s.t. if (v, v ′ ) ∈ E then C(v) = C(v ′ ).
Define the mask M by M (a) = C(a) for a ∈ V . We claim that A G is ((M, n), 1)-diagnosable (thus, also (M, n)-diagnosable). Assume on the contrary that A G is not ((M, n), 1)-diagnosable. Then there exist two runs ρ ∈ Faulty ≥1 (A G ) and ρ ′ ∈ NonFaulty(A G ) such that M * (π /Σ (tr(ρ))) = M * (π /Σ (tr(ρ ′ ))). As ρ is 1-faulty it must be of the form ρ

= v 1 .ε.u 1 • • • u i .f.v i .ε k with 1 ≤ i ≤ j and k ≥ 0. Notice that M (a) = ε for all a ∈ V . Hence it implies M * (π /Σ (tr(ρ))) = M (v 1 ).M (u 1 ) • • • M (u i ).M (v i ), and |M * (π /Σ (tr(ρ)))| = 2i. Consequently, |M * (π /Σ (ρ ′ ))| = 2i. The only possi- ble such ρ ′ which is non-faulty is ρ ′ = v 1 .ε.u 1 • • • v i .ε.u i . Now, M * (π /Σ (tr(ρ))) = M * (π /Σ (tr(ρ ′ ))), which implies M (v i ) = M (u i ) i.e. C(v i ) = C(u i ). But (u i , v i ) ∈ E,
and this contradicts the assumption that C is a valid coloring.

Dynamic Observers

In this section we introduce dynamic observers. To illustrate why dynamic observers can be useful consider the following example.

Example 3 (Dynamic Observation) Assume we want to detect faults in automaton B of Figure 3. A static diagnoser that observes Σ = {a, b} works, however, no proper subset of Σ can be used to detect faults in B. Thus the minimum cardinality of the set of observable events for diagnosing B is 2 i.e. a static observer will have to monitor two events during the execution of the DES. If we want to use a mask, the minimum-cardinality for a mask is 2 as well. This means that an observer will have to be receptive to at least two inputs at each point in time to detect a fault in B. One can think of being receptive as switching on a device to sense an event. This consumes energy. We can be more efficient using a dynamic observer, that only turns on sensors when needed, thus saving energy. In the case of B, this can be done as follows: in the beginning we only switch on the asensor; once an a occurs the a-sensor is switched off and the b-sensor is switched on. Compared to the previous diagnosers we use half as much energy.

• • • • • • ε ε f a b b a

Dynamic Observers

We formalize the above notion of dynamic observation using observers. The choice of the events to observe can depend on the choices the observer has made before and on the observations it has made. Moreover an observer may have unbounded memory. Definition 4 (Observer) An observer Obs over Σ is a deterministic labeled automaton Obs = (S, s 0 , Σ, δ, L), where S is a (possibly infinite) set of states, s 0 ∈ S is the initial state, Σ is the set of observable events, δ : S×Σ → S is the transition function (a total function), and L : S → 2 Σ is a labeling function that specifies the set of events that the observer wishes to observe when it is at state s. We require for any state s and any a ∈ Σ, if a ∈ L(s) then δ(s, a) = s: this means the observer does not change its state when an event it has chosen not to observe occurs. We use the notation δ(s 0 , w) to denote the state s reached after reading the word w and L(δ(s 0 , w)) is the set of events obs observes after w.

An observer implicitly defines a transducer that consumes an input event a ∈ Σ and, depending on the current state s, either outputs a (when a ∈ L(s)) and moves to a new state δ(s, a), or outputs ε, (when a ∈ L(s)) and remains in the same state waiting for a new event. Thus, an observer defines a mapping Obs from Σ * to Σ * (we use the same name "Obs" for the automaton and the mapping). Given a run ρ, Obs(π /Σ (tr(ρ))) is the output of the transducer on ρ. It is called the observation of ρ by Obs. We next provide an example of a particular case of observer which can be represented by a finite-state machine. 0

L(0) = {a} 1 L(1) = {b} 2 L(2) = ∅

Fault Diagnosis with Dynamic Diagnosers

Definition 5 ((Obs, k)-diagnoser) Let A be a finite automaton over Σ ε,f and Obs be an observer over Σ. D :

Σ * → {0, 1} is an (Obs, k)-diagnoser for A if (i) ∀ρ ∈ NonFaulty(A), D(Obs(π /Σ (tr(ρ)))) = 0 and (ii) ∀ρ ∈ Faulty ≥k (A), D(Obs(π /Σ (tr(ρ)))) = 1. A is (Obs, k)-diagnosable if there is an (Obs, k)-diagnoser for A. A is Obs-diagnosable if there is some k such that A is (Obs, k)-diagnosable.
If a diagnoser always selects Σ as the set of observable events, it is a static observer and (Obs, k)-diagnosability amounts to the standard (Σ, k)-diagnosis problem [START_REF] Sampath | Teneketzis. Diagnosability of discrete event systems[END_REF]. In this case A is (Σ, k)-diagnosable iff equation (1) holds.

As for Σ-diagnosability, we have the following equivalence for dynamic observers: A is (Obs, k)-diagnosable iff Obs(π /Σ (Faulty tr ≥k (A))) ∩ Obs(π /Σ (NonFaulty tr (A))) = ∅. This follows directly from definition 5.

Problem 3 (Finite-State Obs-Diagnosability)

INPUT: A, Obs a finite-state observer. PROBLEM:

(A) Is A Obs-diagnosable? (B) If the answer to (A) is "yes", compute the minimum k such that A is (Obs, k)-diagnosable.
Theorem 3 Problem 3 is in P.

Proof: (Sketch) The proof runs as follows: we build a product automaton 3 A ⊗ Obs such that:

A is (Obs, k)- diagnosable ⇐⇒ A ⊗ Obs is (Σ, k)-diagnosable. Let A = (Q, q 0 , Σ ε,f , →
) be a finite automaton and Obs = (S, s 0 , Σ, δ, L) be a finite-state observer. We define the automaton A ⊗ Obs = (Q × S, (q 0 , s 0 ), Σ ε,f , →) as follows:

• (q, s)

β -→ (q ′ , s ′ ) iff ∃λ ∈ Σ s.t. q λ -→ q ′ , s ′ = δ(s, λ) and β = λ if λ ∈ L(s), β = ε otherwise; • (q, s) λ -→ (q ′ , s) iff ∃λ ∈ {ε, f } s.t. q λ -→ q ′ .
As the size of A ⊗ Obs is polynomial in the size of A and Obs the result follows.

For Problem 3, we have assumed that an observer was given. It would be even better if we could synthesize an observer Obs such that the plant A is diagnosable. Before attempting to synthesize such an observer, we should first check that the plant is Σ-diagnosable: if it is not, then obviously no such observer exists; if the plant is Σ-diagnosable, then the trivial observer that observes all events in Σ at all times works 4 . Therefore, we need a way to compute all the "good" observers. Hence we define the problem of computing the set of all valid observers.

Problem 4 (Dynamic-Diagnosability)

INPUT: A. PROBLEM: Compute the set O of all observers such that A is Obs-diagnosable iff Obs ∈ O.
We do not have a solution to the above problem: it can be reduced to finding a trace-based winning strategy for a Büchi game with partial observation. To do this, we use a Büchi objective instead of a safety objective in the construction given in section 5.3. We know how to do this for safety games (Appendix B in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF]) but we do not have a solution to solve Büchi games of this type. Instead, we introduce a restricted variant:

Problem 5 (Dynamic-k-Diagnosability) INPUT: A, k ∈ N. PROBLEM: Compute the set O of all observers such that A is (Obs, k)-diagnosable iff Obs ∈ O.

Problem 5 as a Game Problem

To solve Problem 5 we reduce it to a safety 2-player game. The definitions and results for such games are given in appendix B in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF]. We also provide an intuitive explanation of such games in this section, as we construct our reduction proof. In short, the reduction we propose is the following:

• Player 1 chooses the set of events it wishes to observe, then it hands over to Player 2;

• Player 2 chooses an event and tries to produce a run which is the observation of a k-faulty run and a nonfaulty run.

Player 2 wins if he can produce such a run. Otherwise Player 1 wins. Player 2 has complete information of Player 1's moves (i.e. , it can observe the sets that Player 1 chooses to observe). Player 1, on the other hand, only has partial information of Player 2's moves because not all events are observable (details follow). Let A = (Q, q 0 , Σ ε,f , →) be a finite automaton. To define the game, we use two copies of automaton A: A k 1 and A 2 . The accepting states of A k 1 are those corresponding to runs of A which are faulty and where more than k steps occurred after the fault. A 2 is a copy of A where the f -transitions have been removed. The game we are going to play is the following:

1. the game starts in an state (q 1 , q 2 ) corresponding to the initial state of the product of A k 1 and A 2 . Initially, it is Player 1's turn to play. Player 1 chooses a set of events he is going to observe i.e. a subset X of Σ and hands it over to Player 2;

assume the automata A k

1 and A 2 are in states (q 1 , q 2 ). Player 2 can change the state of A k 1 and A 2 by: (a) firing an action which is not in X in either A k 1 or A 2 (no synchronization). In this case a new state (q, q ′ ) is reached and Player 2 can play again from this state;

(b) firing an action λ in X: to do this both A k 1 and A 2 must be in a state where λ is possible (synchronization); after the action is fired a new state (q ′ 1 , q ′ 2 ) is reached: now it is Player 1's turn to play, and the game continues as in step 1 above from the new state (q ′ 1 , q ′ 2 ).

Player 2 wins if he can reach a state (q 1 , q 2 ) in A k 1 × A 2 where q 1 is an accepting state of A k 1 (this means that Player 1 wins if it can avoid ad infinitum this set of states). In this sense this is a safety game for Player 1 (and a reachability game for Player 2).

Formally, the game G A = (S 1 ⊎ S 2 , s 0 , Σ 1 ⊎ Σ 2 , δ) is defined as follows (⊎ denotes union of disjoint sets):

• S 1 = (Q × {-1, • • • , k}) × Q is the set of Player 1
states; a state ((q 1 , j), q 2 ) ∈ S 1 indicates that A k 1 is in state q 1 , j steps have occurred after a fault, and q 2 is the current state of A 2 . If no fault has occurred, j = -1 and if more than k steps occurred after the fault, we use j = k.

• S 2 = (Q×{-1, • • • , k})×Q×2 Σ is the set of Player 2
states. For a state ((q 1 , j), q 2 , X) ∈ S 2 , the triple ((q 1 , j), q 2 ) has the same meaning as for S 1 , and X is the set of moves Player 1 has chosen to observe on its last move.

• s 0 = ((q 0 , -1), q 0 ) is the initial state of the game belonging to Player 1;

• Σ 1 = 2 Σ is the set of moves of Player 1; Σ 2 = Σ ε is the set of moves of Player 2 (as we encode the fault into the state, we do not need to distinguish f from ε).

• the transition relation δ ⊆ (S 1 × Σ 1 × S 2 ) ∪ (S 2 × {ε} × S 2 ) ∪ (S 2 × Σ × S 1
) is defined by:

-Player 1 moves: let σ ∈ Σ 1 and s 1 ∈ S 1 . Then (s 1 , σ, (s 1 , σ)) ∈ δ.

-Player 2 moves: a move of Player 2 is either a silent move (ε) i.e. a move of A k 1 or A 2 or a joint move of A k 1 and A 2 with an observable action in X. Consequently, a silent move ((q 1 , i), q 2 , X), ε, (q ′ 1 , j), q ′ 2 , X)) is in δ if one of the following conditions holds:

1. either q ′ 2 = q 2 , q 1 ℓ -→ q ′ 1 is a step of A k 1 , ℓ ∈ X, and if i ≥ 0 then j = min(i + 1, k); if i = -1 and ℓ = f j = 0 otherwise j = i.

either q

′ 1 = q 1 , q 2 ℓ -→ q ′ 2 is a step of A 2 , ℓ ∈ X (and ℓ = f ), and if i ≥ 0 then j = min(i + 1, k), otherwise j = i.
A visible move can be taken by Player 2 if both A k 1 and A 2 agree on doing such a move. In this case the game proceeds to a Player 1 state:

((q 1 , i), q 2 , X), ℓ, ((q ′ 1 , j), q ′ 2 )) ∈ δ if ℓ ∈ X, q 1 ℓ -→ q ′ 1 is a step of A k 1 , q 2 ℓ -→ q ′
2 is a step of A 2 , and if i ≥ 0 then j = min(i + 1, k), otherwise j = i.

We can show that for any observer O s.t. A is (O, k)diagnosable, there is a strategy f (O) for Player 1 in G A s.t. f (O) is trace-based and winning. A strategy for Player 1 is a mapping f : Runs(G A ) → Σ 1 that associates a move f (ρ) in Σ 1 to each run ρ in G A that ends in an S 1state. A strategy f is trace-based (see appendix B in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] for details), if given two runs ρ, ρ ′ , if tr(ρ) = tr(ρ ′ ) then f (ρ) = f (ρ ′ ). Conversely, for any trace-based winning strategy f (for Player 1), we can build an observer O(f )

s.t. A is (O(f ), k)-diagnosable.
Let O = (S, s 0 , Σ, δ, L) be an observer for A. We define the strategy f (O) on finite runs of G A ending in a Player 1 state by: f (O)(ρ) = L(δ(s 0 , π /Σ (tr(ρ)))). The intuition is that we take the run ρ in G A , take the trace of ρ (choices of Player 1 and moves of Player 2) and remove the choices of Player 1. This gives a word in Σ * . The strategy for Player 1 for ρ is the set of events the observer O chooses to observe after reading π /Σ (tr(ρ)) i.e. L(δ(s 0 , π /Σ (tr(ρ)))).

Theorem 4 Let O be an observer s.t. A is (O, k)-dia- gnosable. Then f (O) is a trace-based winning strategy in G A .
Proof: First f (O) is trace-based by definition. We have to prove that f (O) is winning. We denote Out(G, f ) the set of outcomes i.e. the set of possible runs of a game G when the strategy f is played by Player 1 (see Appendix B in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] for a formal definition of Out(G, f )). Assume on the contrary that f (O) is not winning. This implies that there is a run ρ in Out(G A , f (O)) as defined by equations (2-5). Each step i of the run given by one of equations (2-5) consists of a choice of Player 1 (X i move) followed by a number of moves by Player 1 (λ j i actions). The last state encountered in ρ, ((q 1 n (α), k n (α)), q 2 n (α), X n ) is a losing state for Player 1, which means that k n (α) ≥ k, by definition of losing states in G A . From the run ρ, we can build two runs ν and ν ′ defined by equations ( 6) and [START_REF] Jiang | Optimal sensor selection for discrete event systems with partial observation[END_REF]. By definition of G A , each λ j i is either a common visible action of A k 1 and A 2 and it is in Σ, or a silent action (ε) i.e. it comes from an action of A k 1 or A 2 that is not in the current set of visible actions X i . We remove from ν (resp. ν ′ ) the actions ε that are obtained from an action of A 2 (resp. A k 1 ) leaving the state of A k 1 (resp. A 2 ) unchanged. Let ν and ν′ be the runs obtained this way. By definition of G A , ν ∈ Faulty ≥k (A) and ν′ ∈ NonFaulty(A). We claim that O(ν) = O(ν ′ ). Indeed, each part of the runs from q

1 i • • • q 1 i+1 and q 2 i • • • q 2 i+1
yields the same observation by O: it is the sequence of events λ j1 • • • λ jn i s.t. each λ j l is a letter of both A k 1 and A 2 and is in X i . As there are two runs ν ∈ Faulty ≥k (A) and ν′ ∈ NonFaulty(A) with the same observation, A is not (O, k)-diagnosable which contradicts the assumption. Hence f (O) must be winning.

Conversely, with each trace-based strategy f of the game G A we can associate an automaton O(f ) = (S, s 0 , Σ, δ, L) defined by:

• S = {π /Σ (tr(ρ)) | ρ ∈ Out(G A , f ) and tgt(ρ) ∈ S 1 }; • s 0 = ε; • δ(v, ℓ) = v ′ if v ∈ S, v ′ = v.ℓ and there is a run ρ ∈ Out(G A , f ) with ρ = q 0 X0 --→ q 1 0 ε * -→ q n0 0 λ1 -→ q 1 X1 --→ q 1 1 ε * -→ q n1 1 λ2 -→ q 2 • • • q k1 ε * -→ q n k-1 k-1 λ k -→ q k with each q i ∈ S 1 , q j i ∈ S 2 , v = π /Σ (tr(ρ)), and ρ X k --→ q 1 k ε * -→ q n k k ℓ -→ q k+1 with q k+1 ∈ S 1 , ℓ ∈ X k . δ(v, l) = v if v ∈ S and ℓ ∈ f (ρ); • L(v) = f (ρ) if v = π /Σ (tr(ρ)). Lemma 1 O(f ) is an observer. Proof: We first have to prove that O(f ) (more precisely L) is well defined. Assume v = π /Σ (tr(ρ)) and v ′ = π /Σ (tr(ρ ′ )). As f is trace-based, f (ρ) = f (ρ ′ )
and there is a unique value for L(v).

We also have to prove that the last requirement of Definition 4 is satisfied i.e. if a ∈ L(s) then δ(s, a) = s. 1. Player 1 chooses the set X 0 = O(f )(ε) which is by definition equal to f ((q 1 0 , -1), q 2 0 ) where ((q 1 0 , -1), q 2 0 ) is the initial state of the game.

2. Player 2 plays the sequence of actions in w 1 and w ′ 1 synchronizing on the common actions of w 1 and w ′ 1 . The game moves through S 2 states because each action is an invisible move. Finally Player 2 chooses λ 0 ∈ O(f )(ε). The game reaches a new S 1 -state ((q 1 1 , k 1 ), q 2 1 ).

3. from ((q 1 1 , k 1 ), q 2 1 ), the strategy f is to play X 1 which by definition is O(f )(λ 0 ). Thus Player 2 can play the sequence of actions given in w 2 and w ′ 2 synchronizing again on common action. In the end Player 2 plays λ 1 ∈ O(f )(λ 0 ).

Conclusion and Future Work

In this paper we have addressed sensor minimization problems in the context of fault diagnosis, using both static and dynamic observers. We showed that computing the smallest number of observable events necessary to achieve diagnosis with a static observer is NP-complete: this result also holds in the mask-based setting which allows to consider events that are observable but not distinguishable. We then focused on dynamic observers and proved that, for a given such observer, diagnosability can be checked in polynomial time (as in the case of static observers). We also solved the synthesis problem of dynamic observers and showed that a most-permissive dynamic observer can be computed in doubly-exponential time.

We are currently investigating the following directions:

• Problem 4 has not been solved so far. The major impediment to solve it is that the reduction we propose in section 5 yields a Büchi game. The algorithm we give in appendix B in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF], does not work for Büchi games and cannot be extended trivially.

• Problem 5 is solved in doubly exponential time. To reduce the number of states of the most permissive observer, we point out that only minimal sets of events we need to be observed. Indeed, if we can diagnose a system by observing only A from some point on, we surely can diagnose it using any superset A ′ ⊇ A. So far we keep all the sets that can be used to diagnose the system. We could possibly take advantage of the previous property using techniques described in [START_REF] Doyen | Algorithms for omega-regular games with imperfect information[END_REF].

• Another line of work is to define a notion of cost for dynamic observers. This can be done and an optimal observer can be computed as it is reported in [START_REF] Cassez | Synthesis of optimal-cost dynamic diagnosers for fault diagnosis of discrete-event systems[END_REF].

  b, c, d}, n = 2 and M (a) = M (b) = 1, M (c) = 2, M (d) = ε, then we have M * (a.b.c.b.d) = 1.1.2.1 = M * (a.a.d.c.a).

Example 2

 2 However, a positive answer to Problem 2(A) does not necessarily imply a positive answer to Problem 1(A), as shown by the example that follows. Consider again the automaton A of Figure 1. Let M (a) = M (b) = 1.

Figure 3 .

 3 Figure 3. The automaton B

Figure 4 . A finite-state observer Obs Example 4

 44 Figure 4. A finite-state observer Obs Example 4 Let Obs be the observer of Figure 4 that maps the following inputs as follows: Obs(baab) = ab, Obs(bababbaab) = ab, Obs(bbbbba) = a and Obs(bbaaa) = a. If Obs operates on the DES B of Figure 3 and B generates f.a.b, Obs will have as input π /Σ (f.a.b) = a.b with Σ = {a, b}. Consequently the observation of Obs is Obs(π /Σ (f.a.b)) = a.b.

Theorem 5

 5 If ℓ ∈ L(v), then ℓ ∈ f (π /Σ (tr(ρ))) for any ρ s.t. v = π /Σ (tr(ρ)) because f is trace-based. Thus δ(v, ℓ) = v. Let f be a trace-based winning strategy in G A . Then A is (O(f ), k)-diagnosable. Proof: Assume A is not (O(f ), k)-diagnosable. There are two runs ν ∈ Faulty ≥k (A) and ν ′ ∈ NonFaulty(A) s.t. O(f )(π /Σ (tr(ν))) = O(f )(π /Σ (tr(ν ′ ))). Let ν (resp.ν′ ) be the sequence of labels that appear in ν (resp. ν ′ ). We can write ν and ν′ in the formν = w -1 λ 0 w 0 λ 1 w 1 • • • λ n w n and ν′ = w ′ -1 λ 0 w ′ 0 λ 1 w ′ 1 • • • λ n w ′ n with w i , w ′ i ∈ (Σ \ O(f )(λ 0 λ 1 • • • λ i ) * for i ≥ 0 and w -1 , w ′ -1 ∈ (Σ \ O(f )(ε)) * , and λ i+1 ∈ O(f )(λ 0 λ 1 • • • λ i ).We build a run in Out(G A , f ) as follows:

In this paper we only use finite automata that generate prefix-closed languages, hence we do not need to use a set of final or accepting states.

Notice that knowing n 0 does not imply we know the required set of observable events Σo! We can find (one of the possibly many) Σo by searching over all possible subsets Σo of Σ of size n 0 (there are C(|Σ|, n 0 ) such combinations) and check for each such Σo whether A is Σo-diagnosable, using the methods described in the appendix A of[START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF].

We use ⊗ to clearly distinguish this product from the synchronous product ×.

Notice that this also shows that existence of an observer implies existence of a finite-state observer, since the trivial observer is finite-state.

Acknowledgments. The authors wish to thank the anonymous referees for their detailed and helpful comments.

* Work supported by the French government project ACI-CORTOS http://www.lsv.ens-cachan.fr/aci-cortos

ρ = (q 1 0 , -1), q 2 0 X0 --→ (q 1 0 , 0), q 2 0 , X 0 λ 1 0 -→ (q 1 0 (1), k 0 (1)), q 2 0 (1), X 0 • • • (q 1 0 (j), k 0 (j)), q 2 0 (j),

(q 1 1 , k 1 ), q 2 1 X1 --→ (q 1 1 , k 1 ), q 2 1 , X 1

We can iterate the previous algorithm and build a run in Out(G A , f ) that reaches a state ((q 1 n , k n ), q 2 n ) with k n ≥ k and thus Out(G A , f ) contains a losing run. Hence f is not winning which contradicts the assumption. This way we conclude that

The result on G A (Appendix B in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF]) is that, if there is a winning trace-based strategy for Player 1, then there is a most permissive strategy F A which has finite memory. It can be represented by a finite automaton

Most Permissive Observer

We now define the notion of a most permissive observer and show the existence of a most permissive observer for a system in case A is diagnosable. F A is the mapping defined at the end of the previous section.

For an observer O = (S, s 0 , Σ, δ, L) and w ∈ Σ * we let L(w) be the set L(δ(s 0 , w)): this is the set of events O chooses to observe on input w. Given a word

.a k i.e. ρ contains the history of what O has chosen to observe at each step and the events that occurred after each choice.

Let O : (2

. By definition O is the most permissive observer for (A, k) if the following holds:

The definition of the most permissive observer states that:

• any good observer O (one such that A is (O, k)diagnosable) must choose a set of observable events in O(w) on input w;

• if an observer chooses its set of observable events in O(w) on input w, then it is a good observer.

Assume A is (Σ, k)-diagnosable. Then there is an observer O s.t. A is (O, k)-diagnosable because the constant observer that observes Σ is a solution. By Theorem 4, there is a trace-based winning strategy for Player 1 in G A . As said at the end of the previous subsection, in this case there is a most permissive trace-based winning strategy which is F A . Theorem 6 F A is the most permissive observer.

Proof: Let O = (S, s 0 , Σ, δ, L) be an observer such that A is (O, k)-diagnosable. We have to prove that L(δ(s 0 , w)) ∈ F A (w) for any w ∈ Σ * . By Theorem 4, the strategy f (O) is a winning trace-based strategy and this implies that f (O)(ν) ∈ F A (ν) for any run ν of G A . By definition of w, π /Σ (w) = w. By definition of f (O), f (O)(w) = L(δ(s 0 , π /Σ (tr(w)))) = L(δ(s 0 , w)) and thus L(δ(s 0 , w)) ∈ F A (w).

Conversely, assume O is such that ∀w ∈ Σ * , L(s 0 , w) ∈ F A (w). We have to prove that A is (O, k)-diagnosable. Again, we build f (O). As before, f (O) is a winning trace-based strategy in G A and thus O

This enables us to solve Problem 5 and compute a finite representation of the set O of all observers such that A is (O, k)-diagnosable iff O ∈ O.

Computing F A can be done in O(2 |GA| ) (Appendix in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF]). The size of G A is quadratic in |A|, linear in the size of k, and exponential in the size of Σ i.e. |G A | = O(|A| 2 × 2 |Σ| × |k|). This means that computing F A can be done in exponential time in the size of A and k and doubly exponential time in the size of Σ.