Search

Artificial intelligence (AI) technologies are increasingly creeping into the work sphere, thereby gradually questioning and/or disturbing the long-established moral concepts and norms communities have been using to define what makes work good. Each community, and Muslims make no exception in this regard, has to revisit their moral world to provide well-thought frameworks that can engage with the challenging ethical questions raised by the new phenomenon of AI-mediated work. For a systematic analysis of the broad topic of AI-mediated work ethics from an Islamic perspective, this article focuses on presenting an accessible overview of the "moral world" of work in the Islamic tradition. Three main components of this moral world were selected due to their relevance to the AI context, namely (1) Work is inherently good for humans, (2) Practising a religiously permitted profession and (c) Maintaining good relations with involved stakeholders. Each of these three components is addressed in a distinct section, followed by a sub-section highlighting the relevance of the respective component to the particular context of AI-mediated work. The article argues that there are no unsurmountable barriers in the Islamic tradition against the adoption of AI technologies in work sphere. However, important precautions should be considered to ensure that embracing AI will not be at the cost of work-related moral values. The article also highlights how important lessons can be learnt from the positive historical experience of automata that thrived in the Islamic civilization. [ABSTRACT FROM AUTHOR]

Runtime Enforcement (RE) is a technique aimed at monitoring the executions of a system at runtime and ensure its compliance against a set of formal requirements (properties). RE employs an enforcer (a safety wrapper for the system) which modifies the (untrustworthy) output by performing actions such as delaying (by storing/buffering) and suppressing events, when needed. In this paper, to handle practical applications with memory constraints, we propose a new RE paradigm where the memory of the enforcer is bounded/finite. Besides the property to be enforced, the user specifies a bound on the enforcer memory. Bounding the memory poses various challenges such as how to handle the situation when the memory is full, how to optimally discard events from the buffer to accommodate new events and let the enforcer continue operating. We define the bounded-memory RE problem and develop a framework for any regular property. All of our results are formalized and proved. We also analyze probabilistically how much memory is required on an average case for a given regular property, such that the output of the bounded enforcer is equal to that of the unbounded enforcer up to a fixed probability. The proposed framework is implemented and a case study is worked out to show the practicability and usefulness of the bounded enforcer in the real-world and to show the usage of the aforementioned probabilistic analysis on them. The performance is evaluated via some examples from application scenarios and it indicates linear changes in the execution time of the enforcers in response to increases in trace length, property complexity, and buffer sizes. [ABSTRACT FROM AUTHOR]

We consider the problem of extracting a deterministic finite automaton (DFA) from a trained recurrent neural network (RNN). We present a novel algorithm that uses exact learning and abstract interpretation to perform efficient extraction of a minimal DFA describing the state dynamics of a given RNN. We use Angluin's L ∗ algorithm as a learner and the given RNN as an oracle, refining the abstraction of the RNN only as much as necessary for answering equivalence queries. Our technique allows DFA-extraction from the RNN while avoiding state explosion, even when the state vectors are large and fine differentiation is required between RNN states. We experiment on multi-layer GRUs and LSTMs with state-vector dimensions, alphabet sizes, and underlying DFA which are significantly larger than in previous DFA-extraction work. Aditionally, we discuss when it may be relevant to apply the technique to RNNs trained as language models rather than binary classifiers, and present experiments on some such examples. In some of our experiments, the underlying target language can be described with a succinct DFA, yet we find that the extracted DFA is large and complex. These are cases in which the RNN has failed to learn the intended generalisation, and our extraction procedure highlights words which are misclassified by the seemingly "perfect" RNN. [ABSTRACT FROM AUTHOR]

According to the principles of compositional verification, verifying that lower-level components satisfy their specification ensures that the whole system satisfies its top-level specification. The key step is to ensure that the lower-level specifications constitute a correct decomposition of the top-level specification. In a non-stochastic context, such decomposition can be analyzed using techniques of theorem proving. In industrial applications, especially in safety-critical systems, specifications are often of stochastic nature, for example, giving a bound on the probability that a system failure will occur before a given time. A decomposition of such a specification requires techniques beyond traditional theorem proving. The first contribution of the paper is a theoretical framework that allows the representation of, and reasoning about, stochastic and timed behavior of systems as well as specifications for such behavior. The framework is based on traces that describe the continuous-time evolution of a system, and specifications are formulated using timed automata combined with probabilistic acceptance conditions. The second contribution is a novel approach to verifying decompositions of such specifications by reducing the problem to checking emptiness of the solution space for a system of linear inequalities. [ABSTRACT FROM AUTHOR]

Intelligent Transport System (ITS) is a typical class of Cyber-Physical Systems (CPS), and due to the special characteristics of such systems, higher requirements are placed on system security. Runtime verification is a lightweight verification technique which is used to improve the security of such systems. However, current runtime verification methods often ignore the effects of the physical environment (e.g., the effects of rain, snow, and other weather changes on road conditions), which results in the inability of the monitor to effectively monitor the system according to the changes in the environment. To address this problem, this paper proposes a method for constructing a runtime monitor with environmental context-awareness capability. First, the physical environment factors affecting the system are formally described and constructed into an environment model, then the system statute is transformed into a Büchi automaton, and then a synthesis algorithm combining the environment model and the Büchi automaton is designed based on the network of automatons, and the corresponding monitor is generated. Finally, the proposed method is applied and verified on simulation and real objects. The experimental results show that the monitors generated based on the method of this paper can effectively monitor unsafe events in different environments, thus improving the safety of intelligent driving systems. [ABSTRACT FROM AUTHOR]

I propose a version of quantum mechanics featuring a discrete and finite number of states that is plausibly a model of the real world. The model is based on standard unitary quantum theory of a closed system with a finite-dimensional Hilbert space. Given certain simple conditions on the spectrum of the Hamiltonian, Schrödinger evolution is periodic, and it is straightforward to replace continuous time with a discrete version, with the result that the system only visits a discrete and finite set of state vectors. The biggest challenges to the viability of such a model come from cosmological considerations. The theory may have implications for questions of mathematical realism and finitism. [ABSTRACT FROM AUTHOR]

It is known that for some languages quantum finite automata are more efficient than classical counterparts. Particularly, a QFA recognizing the language has an exponential advantage over the classical finite automata. However, the construction of such QFA is probabilistic. In the current work, we propose a deterministic construction of the QFA for the language . We construct a QFA for a promise problem and implement this QFA on the IBMQ simulator using qiskit library tools. [ABSTRACT FROM AUTHOR]

Infectious diseases are transmitted from one person to another and spread throughout a network under certain conditions. Considering an example of propagation, we explain how to define an automaton on the network according to the propagation steps and the conditions under which the epidemic is transmitted. We call this automaton forcing automaton. Also, we call the language of this automaton an epidemic language. We describe how forcing automata and epidemic languages allow us to have a more accurate analysis of propagation in reality. Furthermore, we show that by knowing the epidemic language, it is possible to compare the spread of an epidemic in different networks. Finally, we present an algorithm that can predict a network in which the epidemic spreads, by only knowing its epidemic language. [ABSTRACT FROM AUTHOR]

Finite automata with counters are often used to specify families of constraints. The addition of counters provides more power than membership in regular languages that is possible with finite automata. All available propagation algorithms for counter automata based constraints maintain only bounds consistency on counter variables, and although it is possible to maintain domain consistency it can be computationally very costly. In this paper we give an algorithm that decides when maintaining bounds consistency for an automata with a single counter implies domain consistency. [ABSTRACT FROM AUTHOR]

This paper describes a technique for solving temporal-logic queries over finite sets of finite-length data streams. Such data streams arise in many domains, including server logs, program testing, and financial and marketing data; temporal-logic formulas that are satisfied by all data streams in a set can provide insight into the underlying dynamics of the system generating the streams. Our approach to finding such formulas is based on solving queries, or formulas that include an unknown, given in a variant of linear temporal logic (LTL). Solving such a query involves computing all propositional formulas that, when substituted for the unknown in the query, yield an LTL formula satisfied by all data streams in the set. We give an automaton-based approach to solving these queries and demonstrate a working implementation via a pilot study. [ABSTRACT FROM AUTHOR]

Self modifying code is code that can modify its own instructions during the execution of the program. It is extensively used by malware writers to obfuscate their malicious code. Thus, analysing self modifying code is nowadays a big challenge. In this paper, we consider the LTL model-checking problem of self modifying code. We model such programs using self-modifying pushdown systems, an extension of pushdown systems that can modify its own set of transitions during execution. We reduce the LTL model-checking problem to the emptiness problem of self-modifying Büchi pushdown systems. We implemented our techniques in a tool that we successfully applied for the detection of several self-modifying malware. Our tool was also able to detect several malwares that well-known antiviruses such as BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Baidu, Avast, and Symantec failed to detect. [ABSTRACT FROM AUTHOR]

Automata theory is one of the branches of mathematical cybernetics, that studies information transducers that arise in many applied problems. The major objective of automata theory is to develop methods by which one can describe and analyze the dynamic behavior of discrete systems. Depending on study tasks, automata are considered, for which the set of states and the set of output signals are equipped with additional mathematical structures preserved by the transition and output functions of automata. In this paper, we investigate automata over graphs and call them graphic automata. For graphs a universal graphic automaton is the universally attracted object in the category of graphic automata, for which the set of states is equipped with the structure of the graph and the set of output signals is equipped with the structure of the graph . The input signal semigroup of the universal graphic automaton is . It may be considered as a derived algebraic system of the mathematical object . It is common knowledge that properties of the semigroup are closely interconnected with properties of the algebraic structure of the automaton. This suggests that universal graphic automata may be researched using their input signal semigroups. In this article, we investigate the concrete characterization problem of graphic automata over reflexive graphs. The main result of our study states necessary and sufficient conditions for an automaton to be a universal graphic automaton over reflexive graphs. [ABSTRACT FROM AUTHOR]

The main drawback of implementing the traditional diagnoser for Discrete-Event Systems proposed in the literature is that its state set can be very large, requiring the use of a large amount of memory to store the diagnoser for complex systems. In this paper, we propose a greedy algorithm for the computation of a reduced diagnoser, that preserves the diagnosability of the system language and the same diagnosis delay as the original diagnoser. The reduction algorithm is based on merging states of the original diagnoser, and uses a free parameter to choose which and in what order states should be merged with a view to trying to obtain a diagnoser with the smallest possible number of states. [ABSTRACT FROM AUTHOR]

Real life experience has shown that intermittent faults are among the most challenging kinds of faults to detect and isolate, being present in the majority of production systems. Such a concern has made intermittent fault an active area of research in both discrete event and continuous-variable dynamic systems. In this paper, we present a review of the state-of-the art of intermittent fault diagnosability of discrete event systems modeled by finite state automata. To this end, we revisit the main definitions of diagnosability of intermittent faults, and present comparisons between them, consider verification and analysis techniques, and discuss available complexity results. Examples are used throughout the paper to illustrate the reviewed concepts and verification algorithms. We also look ahead, by suggesting some perspectives for future research. [ABSTRACT FROM AUTHOR]

We give two different proofs of the fact that non-oblivious selection via regular group sets preserves normality. Non-oblivious here means that whether or not a symbol is selected can depend on the symbol itself. One proof relies on the incompressibility of normal sequences, the other on the use of augmented dynamical systems. [ABSTRACT FROM AUTHOR]

Since the Nuremberg Code and the first Declaration of Helsinki, globally there has been increasing adoption and adherence to procedures for ensuring that human subjects in research are as well informed as possible of the study's reasons and risks and voluntarily consent to serving as subject. To do otherwise is essentially viewed as violation of the human research subject's legal and moral rights. However, with the recent philosophical concerns about responsible robotics, the limits and ambiguities of research-subjects ethical codes become apparent on the matter of constructing automata that maximally resemble human beings (as defined hereunder). In this case, the automata themselves, as products of research and development, are in the very process of their construction subjects of research and development. However, such research faces a paradox: The subjects cannot give their informed consent to this research for their own development, although their consent would be needed for the research. According to ethical codes, this research would be unethical. The article then explores whether the background concepts giving rise to this paradox could be reframed in order to allow such research to proceed ethically. [ABSTRACT FROM AUTHOR]

Automated techniques and tools for the construction and analysis of systems are inevitable to manage the complexity of the current systems. Such techniques and tools are the subject of interest of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems—TACAS. This special issue of Software Tools for Technology Transfer presents extended versions of five selected papers from the 25th edition of TACAS that took place in 2019. All of the papers included into this special issue aim at various aspects of automated design and formal verification and hence contribute to development of more reliable computer systems. [ABSTRACT FROM AUTHOR]

We equip a recently developed model for the specification of service contracts with real-time constraints. Service contracts offer a means to define the behavioural compliance of a composition of services, typically dictated in a service-level agreement (SLA), as the fulfilment of all service requests through service offers. Depending on their granularity, SLAs vary according to the level of criticality of the involved services and also contain real-time aspects, like the services' response or expiration time. A standard method to refine a spurious service composition into a compliant one is via the synthesis of a safe orchestration, in the form of the most permissive controller from supervisory control theory. Ideally, safe orchestrations solve competition among matching service requests and offers, in light of their criticalities and their timing constraints, in the best possible way. In this paper, we introduce timed service contract automata as a novel formal model for service contracts with real-time constraints on top of services with varying levels of criticality. We also define a means to efficiently compute their composition and their safe orchestration, using the concept of zones from timed games. The innovations of our contribution are illustrated by intuitive examples and by a preliminary evaluation. [ABSTRACT FROM AUTHOR]

We investigate parameterizations of both database instances and queries that make query evaluation fixed-parameter tractable in combined complexity. We show that clique-frontier-guarded Datalog with stratified negation (CFG-Datalog) enjoys bilinear-time evaluation on structures of bounded treewidth for programs of bounded rule size. Such programs capture in particular conjunctive queries with simplicial decompositions of bounded width, guarded negation fragment queries of bounded CQ-rank, or two-way regular path queries. Our result is shown by translating to alternating two-way automata, whose semantics is defined via cyclic provenance circuits (cycluits) that can be tractably evaluated. [ABSTRACT FROM AUTHOR]

Fault tree analysis is still widely practiced in high-hazard industries. We propose in this article an algorithm for the reduction of fault tree expressions that are generated from automata representations of failure behaviors. Automata formalisms are increasingly being used to describe systems exhibiting sequence-dependent failures—i.e., the overall outcome like a total failure of the system can depend on the order in which events occur. A set of paths leading to a safety-relevant state is encoded as a standard sum of product canonical form, and without any loss of the significance of the sequencing of events. That is, the corresponding fault tree expression is basically a Boolean formula which is extended with the necessary temporal features (event occurrence priority). Such expressions can then be reduced into minimal canonical forms by using the Boolean methods together with the required temporal logic calculus. Since minimal failure sequences can be determined from the obtained reduced models, the proposed approach can improve the analysis of the dynamic effects of the sequencing of faults and propagated errors in such models. As a consequence, it can have a positive impact on the design of failure prevention measures. A fault tolerant example system exhibiting dynamic behavior is used to highlight the benefits of the approach. [ABSTRACT FROM AUTHOR]

Modeling all aspects of a complex system within a single model is a difficult, if not impossible, task. Multi-view modeling is a methodology where different aspects of the system are captured by different models, or views. A key question then is consistency: if different views of a system have some degree of overlap, how can we guarantee that they are consistent, i.e., that they do not contradict each other? In this paper we formulate this and other basic problems in multi-view modeling within an abstract formal framework. We then instantiate this framework onto several discrete system settings: languages and automata over finite and infinite words, and symbolic transition systems; and study how checking view consistency and other problems can be solved in these settings. [ABSTRACT FROM AUTHOR]

In this paper, we present a method for discrete event system identification with the aim of fault detection. The method is based on a new model called Deterministic Automaton with Outputs and Conditional Transitions (DAOCT), which is computed from observed fault-free paths, and represents the fault-free system behavior. In practice, a trade-off between size and accuracy of the identified automaton has to be found. In order to obtain compact models, loops are introduced in the model, which implies that sequences that are not observed can be generated by the model leading to an exceeding language. This exceeding language is associated with possible non-detectable faults, and must be reduced in order to use the model for fault detection. We show, in this paper, that the exceeding language generated by the DAOCT is smaller than the exceeding language generated by another model proposed in the literature, reducing, therefore, the number of possible non-detectable faults. We also show that if the identified DAOCT does not have cyclic paths, then the exceeding language is empty, and the model represents all and only all observed fault-free sequences generated by the system. In order to illustrate the results of the paper, a physical system is simulated by using a 3D simulation software controlled by a Programmable Logic Controller (PLC). The main idea is to use a virtual digital system to simulate the fault-free behavior of a physical system, captured by the sequences of input and output signals of the PLC, and then use the method proposed in the paper to obtain the DAOCT model of the plant. [ABSTRACT FROM AUTHOR]

Communication networks are commonly used to connect sensors, actuators, and controllers to monitor and control cyber-physical systems (CPS). The use of communication networks increases the vulnerability of the CPS to cyber attacks that can drive the system to reach unsafe states. One of the most powerful cyber attacks is the so-called man-in-the-middle attack, where the intruder can observe, hide, create or replace information in the attacked network channel. In a previous paper, we have introduced the definition of NA-Safe controllability, that is related with the capability of detecting intrusions and preventing damages caused by man-in-the-middle attacks in the sensor and/or control communication channels in supervisory control systems. In this paper, we extend our previous work as follows: (i) we prove the correctness of the NA-Safe controllability verification algorithm; (ii) we show how to implement the security module against cyber attacks; (iii) we show that NA-Safe controllability is a necessary and sufficient condition for the existence of the security module; and (iv) we present a practical example to illustrate the results of the paper. [ABSTRACT FROM AUTHOR]

Failures in manufacturing systems reliant on human operators must address the issues of coverage, liveness, and starvation (CLS) to prevent accidental interactions among the component of the system or accidental human-automation interaction (HAI). Manufacturing systems would benefit from techniques that lay the ground work for investigating the possible rectifications for problems that might cause down time. The formal verification is the dominant technique utilized, along with mathematical proof that shows that an accordingly scaled model of a manufacturing system contains the desired properties of the large real-world manufacturing systems. This paper describes a method of FSZ-automaton, which combines finite-state machine model with Z-schemas for establishing concurrency and a distributed structure within manufacturing systems. FSZ-automaton was used to complete the formal verification of the part manufacturing system. This formal verification is also used to validate FSZ-automaton, its usability properties, and to distinguish the mode confusion. Moreover, the advances in formal verification continue to address these issues, such that the traditional analysis procedure is validated and can potentially avoid this constraint. [ABSTRACT FROM AUTHOR]

What does it take to implement a computer? Answers to this question have often focused on what it takes for a physical system to implement an abstract machine. As Joslin (Minds Mach 16:29-41, 2006) observes, this approach neglects cases of software implementation—cases where one machine implements another by running a program. These cases, Joslin argues, highlight serious problems for mapping accounts of computer implementation—accounts that require a mapping between elements of a physical system and elements of an abstract machine. The source of these problems is the complexity introduced by common design features of ordinary computers, features that would be relevant to any real-world software implementation (e.g., virtual memory). While Joslin is focused on contemporary views, his discussion also suggests a counterexample to recent mapping accounts which hold that genuine implementation requires simple mappings (Millhouse in Br J Philos Sci, 2017. 10.1093/bjps/axx046; Wallace in The emergent multiverse, Oxford University Press, Oxford, 2014). In this paper, I begin by clarifying the nature of software implementation and disentangling it from closely related phenomena like emulation and simulation. Next, I argue that Joslin overstates the degree of complexity involved in his target cases and that these cases may actually give us reasons to favor simplicity-based criteria over relevant alternatives. Finally, I propose a novel problem for simplicity-based criteria and suggest a tentative solution. [ABSTRACT FROM AUTHOR]

The Parikh automaton model equips a finite automaton with integer registers and imposes a semilinear constraint on the set of their final settings. Here the theories of typed monoids and of rational series are used to characterize the language classes that arise algebraically. Complexity bounds are derived, such as containment of the unambiguous Parikh automata languages in NC1. Affine Parikh automata, where each transition applies an affine transformation on the registers, are also considered. Relying on these characterizations, the landscape of relationships and closure properties of the classes at hand is completed, in particular over unary languages. [ABSTRACT FROM AUTHOR]

The diagnosis problem for discrete event systems consists in deciding whether some fault event occurred or not in the system, given partial observations on the run of that system. Diagnosability checks whether a correct diagnosis can be issued in bounded time after a fault, for all faulty runs of that system. This problem appeared two decades ago and numerous facets of it have been explored, mostly for permanent faults. It is known for example that diagnosability of a system can be checked in polynomial time, while the construction of a diagnoser is exponential. The present paper examines the case of transient faults, that can appear and be repaired. Diagnosability in this setting means that the occurrence of a fault should always be detected in bounded time, but also before the fault is repaired, in order to prepare for the detection of the next fault or to take corrective measures while they are needed. Checking this notion of diagnosability is proved to be PSPACE-complete. It is also shown that faults can be reliably counted provided the system is diagnosable for faults and for repairs. [ABSTRACT FROM AUTHOR]

Recently we proposed relative observability for supervisory control of discrete-event systems under partial observation. Relative observability is closed under set unions and hence there exists the supremal relatively observable sublanguage of a given language. In this paper we present a new characterization of relative observability, based on which an operator on languages is proposed whose largest fixpoint is the supremal relatively observable sublanguage. Iteratively applying this operator yields a monotone sequence of languages; exploiting the linguistic concept of support based on Nerode equivalence, we prove for regular languages that the sequence converges finitely to the supremal relatively observable sublanguage, and the operator is effectively computable. Moreover, for the purpose of control, we propose a second operator that in the regular case computes the supremal relatively observable and controllable sublanguage. [ABSTRACT FROM AUTHOR]

Nanomanipulation plays a significant role in nanotechnology research. The process of Atomic force microscopy (AFM) based manipulation is complex and time-consuming, which can be improved using a path-planning algorithm to reduce its manipulation time and time complexity. Due to real-time monitoring limitation in AFM based manipulations, Virtual reality (VR) environments have been developed. One such developed VR environment, however, is limited to point to point manipulation and lacks any path information. Therefore, we propose using a hybrid Improved particle swarm optimization (IPSO), a cellular automata-based algorithm for path planning during manipulation of micro/nanoparticles. In this technique, the critical time-force diagram, representing the AFM based manipulation dynamic is considered as a constraint, and is subsequently used to find the best path. The main path is divided into several segments and is optimized. Used as an algorithm for manipulation, this technique provides a more precise path in the AFM-based manipulation. Finally, the ability of this technique was compared to the other path planner algorithms based on its efficiency in reducing time-complexity parameters. [ABSTRACT FROM AUTHOR]

A new modeling tool, algebraic state space approach to logical dynamic systems, which is developed recently based on the theory of semi-tensor product of matrices (STP), is applied to the automata field. Using the STP, this paper investigates the modeling and controlling problems of combined automata constructed in the ways of parallel, serial and feedback. By representing the states, input and output symbols in vector forms, the transition and output functions are expressed as algebraic equations of the states and inputs. Based on such algebraic descriptions, the control problems of combined automata, including output control and state control, are considered, and two necessary and sufficient conditions are presented for the controllability, by which two algorithms are established to find out all the control strings that make a combined automaton go to a target state or produce a desired output. The results are quite different from existing methods and provide a new angle and means to understand and analyze the dynamics of combined automata. [ABSTRACT FROM AUTHOR]

Let K be an algebraically closed field of characteristic p. We exhibit a counterexample against a theorem asserted in one of our earlier papers, which claims to characterize the integral closure of K(( t)) within the field of Hahn-Mal'cev-Neumann generalized power series. We then give a corrected characterization, generalizing our earlier description in terms of finite automata in the case where K is the algebraic closure of a finite field. We also characterize the integral closure of K( t), thus generalizing a well-known theorem of Christol and suggesting a possible framework for computing in this integral closure. We recover various corollaries on the structure of algebraic generalized power series; one of these is an extension of Derksen's theorem on the zero sets of linear recurrent sequences in characteristic p. [ABSTRACT FROM AUTHOR]

In the classical synthesis problem, we are given a specification ψ over sets of input and output signals, and we synthesize a finite-state transducer that realizes ψ: with every sequence of input signals, the transducer associates a sequence of output signals so that the generated computation satisfies ψ. In recent years, researchers consider extensions of the classical Boolean setting to a multi-valued one. We study a multi-valued setting in which the truth values of the input and output signals are taken from a finite lattice, and so is the satisfaction value of specifications. We consider specifications in latticed linear temporal logic (LLTL). In LLTL, conjunctions and disjunctions correspond to the meet and join operators of the lattice, respectively, and the satisfaction values of formulas are taken from the lattice too. The lattice setting arises in practice, for example in specifications involving priorities or in systems with inconsistent viewpoints. We solve the LLTL synthesis problem, where the goal is to synthesize a transducer that realizes the given specification in a desired satisfaction value. For the classical synthesis problem, researchers have studied a setting with incomplete information, where the truth values of some of the input signals are hidden and the transducer should nevertheless realize ψ. For the multi-valued setting, we introduce and study a new type of incomplete information, where the truth values of some of the input signals may be noisy, and the transducer should still realize ψ in the desired satisfaction value. We study the problem of noisy LLTL synthesis, as well as the theoretical aspects of the setting, like the amount of noise a transducer may tolerate, or the effect of perturbing input signals on the satisfaction value of a specification. We prove that the noisy-synthesis problem for LLTL is 2EXPTIME-complete, as is traditional LTL synthesis. [ABSTRACT FROM AUTHOR]

Runtime enforcement (RE) is a technique to ensure that the (untrustworthy) output of a black-box system satisfies some desired properties. In RE, the output of the running system, modeled as a sequence of events, is fed into an enforcer. The enforcer ensures that the sequence complies with a certain property, by delaying or modifying events if necessary. This paper deals with predictive runtime enforcement, where the system is not entirely black-box, but we know something about its behavior. This a priori knowledge about the system allows to output some events immediately, instead of delaying them until more events are observed, or even blocking them permanently. This in turn results in better enforcement policies. We also show that if we have no knowledge about the system, then the proposed enforcement mechanism reduces to standard (non-predictive) runtime enforcement. All our results related to predictive RE of untimed properties are also formalized and proved in the Isabelle theorem prover. We also discuss how our predictive runtime enforcement framework can be extended to enforce timed properties. [ABSTRACT FROM AUTHOR]

We introduce the notion of topological entropy of a formal language as the topological entropy of the minimal topological automaton accepting it. Using a characterization of this notion in terms of approximations of the Myhill-Nerode congruence relation, we are able to compute the topological entropies of certain example languages. Those examples suggest that the notion of a 'simple' formal language coincides with the language having zero entropy. [ABSTRACT FROM AUTHOR]

We study those automatic sequences which are produced by an automaton whose underlying graph is the Cayley graph of a finite group. For 2-automatic sequences, we find a characterization in terms of what we call homogeneity, and among homogeneous sequences, we single out those enjoying what we call self-similarity. It turns out that 2-self-similar sequences (viewed up to a permutation of their alphabet) are in bijection with many interesting objects, for example dessins d'enfants (covers of the Riemann sphere with three points removed). For any p, we show that, in the case of an automatic sequence produced 'by a Cayley graph,' the group and indeed the automaton can be recovered canonically from the sequence. Further, we show that a rational fraction may be associated with any automatic sequence. To compute this fraction explicitly, knowledge of a certain graph is required. We prove that for the sequences studied in the first part, the graph is simply the Cayley graph that we start from, and so calculations are possible. We give applications to the study of the frequencies of letters. [ABSTRACT FROM AUTHOR]

Sepsis is a life-threatening condition caused by an inappropriate immune response to infection, and is a leading cause of elderly death globally. Early recognition of patients and timely antibiotic therapy based on guidelines improve survival rate. Unfortunately, for those patients, it is often detected late because it is too expensive and impractical to perform frequent monitoring for all the elderly. In this paper, we present a risk driven sepsis screening and monitoring framework to shorten the time of onset detection without frequent monitoring of all the elderly. Within this framework, the sepsis ultimate risk of onset probability and mortality is calculated based on a novel temporal probabilistic model named Auto-BN, which consists of time dependent state, state dependent property, and state dependent inference structures. Then, different stages of a patient are encoded into different states, monitoring frequency is encoded into the state dependent property, and screening content is encoded into different state dependent inference structures. In this way, the screening and monitoring frequency and content can be automatically adjusted when encoding the sepsis ultimate risk into the guard of state transition. This allows for flexible manipulation of the tradeoff between screening accuracy and frequency. We evaluate its effectiveness through empirical study, and incorporate it into existing medical guidance system to improve medical healthcare. [ABSTRACT FROM AUTHOR]

This paper studies the interaction of automata of size m. We characterise statistical properties satisfied by random plays generated by a correlated pair of automata with m states each. We show that in some respect the pair of automata can be identified with a more complex automaton of size comparable to $$m\log m$$ . We investigate implications of these results on the correlated min-max value of repeated games played by automata. [ABSTRACT FROM AUTHOR]

As engineers propose constructing humanlike automata, the question arises as to whether such machines merit human rights. The issue warrants serious and rigorous examination, although it has not yet cohered into a conversation. To put it into a sure direction, this paper proposes phrasing it in terms of whether humans are morally obligated to extend to maximally humanlike automata full human rights, or those set forth in common international rights documents. This paper's approach is to consider the ontology of humans and of automata and whether ontological difference between them, that pertains to the very bases of human rights, affects the latter's claims to full human rights. Considering common bases of human rights, can these bases tell us whether a certain ontological distinction of humans from automata-or a de facto distinction about humans tacitly acknowledged by full-rights-recognizing societies-makes a difference in whether humans are morally obligated to assign these entities full rights? Human rights to security also arise. The conclusion is that humans need not be under any moral obligation to confer full human rights on automata. The paper's ultimate point is not to close the discussion with this ontological cap but to set a solid moral and legal groundwork for opening it up tout court. [ABSTRACT FROM AUTHOR]

Node selecting tree automata (NSTAs) constitute a general formalism defining unary queries over trees. Basically, a node is selected by an NSTA when it is visited in a selecting state during an accepting run. We consider twig patterns as an abstraction of XPath. Since the queries definable by NSTAs form a strict superset of twig-definable queries, we study the complexity of the problem to decide whether the query by a given NSTA is twig-definable. In particular, we obtain that the latter problem is EXPTIME-complete. In addition, we show that it is also EXPTIME-complete to decide whether the query by a given NSTA is definable by a node selecting string automaton. [ABSTRACT FROM AUTHOR]

This paper presents an extension of the original strange planet protocol with three species who mate in a special way, to $$m$$ species and reveals essential principles in the new protocol. Further, must-fail, might-fail and cannot-fail states are formalized and the relationship among them is established. Moreover, the number of each kind of states is calculated. In addition, the conditions for secure communications based on the new protocol are given. Finally, an application is provided to illustrate how the extended strange planet protocol can be used for secure communication. [ABSTRACT FROM AUTHOR]

Recently we developed supervisor localization, a top-down approach to distributed control of discrete-event systems in the Ramadge-Wonham supervisory control framework. Its essence is the allocation of monolithic (global) control action among the local control strategies of individual agents. In this paper, we start by presenting several refinements of our localization theory. First, we drop the original assumption that the event sets of component agents are pairwise disjoint. Second, we show that consistent marking information can be enforced by just one agent, which can be selected arbitrarily. Third, the event sets of localized controllers are explicitly defined, in general as proper subsets of the entire event set. For these generalizations, we again prove that the collective local controlled behavior is identical to the global optimal and nonblocking controlled behavior. Moreover, we provide a language interpretation of localization by relating the key concept of control cover/congruence on the supervisor's state set to a special right congruence on the supervisor's language.W e go on to apply the extended supervisor localization to solve a multi-agent formation problem. We introduce a suitable formulation of formation invariance as well as shortest paths to formation. Local strategies are synthesized for a group of agents to arrive at a pre-specified formation in shortest paths; then issues of information exchange and control logic are examined. We further demonstrate the extended localization on a large-scale Cluster Tool example. By first synthesizing a set of decentralized supervisors and coordinators by an efficient heterarchical approach, our localization yields a distributed control architecture with comprehensible local control/coordination logic. [ABSTRACT FROM AUTHOR]

A new linear transformation from PLTL formulas to alternating automata is proposed in this paper. To this end, C-F normal forms and normal form graphs (NFGs) are defined for PLTL formulas. Further, based on NFGs, generalized alternating Büchi automata (GABA) of PLTL formulas are built. Beside the conciseness in theoretical aspect, the new transformation is useful in improving the scalability of LTL model checking tools in practise. Also, based on the new transformation, an intuitive on-the-fly model checking approach can be implemented. [ABSTRACT FROM AUTHOR]