Ruggero Lanotte
email: ruggero.lanotte@uninsubria.it

Massimo Merro
email: massimo.merro@univr.it

Andrei Munteanu
email: andrei.munteanu@univr.it

A Modest Security Analysis of Cyber-Physical Systems: A Case Study

Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes. Although the range of applications of CPSs include several critical domains, their verification and validation often relies on simulation-test systems rather then formal methodologies. In this paper, we use a recent version of the expressive MODEST TOOLSET to implement a non-trivial engineering application, and test its safety model checker prohver as a formal instrument to statically detect a variety of cyber-physical attacks, i.e., attacks targeting sensors and/or actuators, with potential physical consequences. We then compare the effectiveness of the MODEST TOOLSET and its safety model checker in verifying CPS security properties when compared to other state-of-the-art model checkers.

3 See [31] for a taxonomy of the time-scale models used to represent CPSs.

Introduction

Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes, where feedback loops allow the latter to affect the computations of the former and vice versa. CPSs have three main components: the physical plant, i.e., the physical process that is managed by the CPS; the logics, i.e., controllers, intrusion detection systems (IDSs), and supervisors that govern and control the physical process; the connecting network.

Historically, CPSs relied on proprietary technologies and were implemented as stand-alone networks in physically protected locations. However, in recent years the situation has changed considerably: commodity hardware, software and communication technologies are used to enhance the connectivity of these systems and improve their operation.

This evolution has triggered a dramatic increase in the number of attacks to the security of cyber-physical and critical systems, e.g., manipulating sensor readings and, in general, influencing physical processes to bring the system into a state desired by the attacker. Some notorious examples are: (i) the Stuxnet worm, which reprogrammed PLCs of nuclear centrifuges in Iran [START_REF] Falliere | [END_REF], (ii) the attack on a sewage treatment facility in Queensland, Australia, which manipulated the SCADA system to release raw sewage into local rivers [START_REF] Slay | Lessons Learned from the Maroochy Water Breach[END_REF], or the (iii) the recent cyber-attack on the Ukrainian power grid, again through the SCADA system [START_REF]ICS-CERT: Cyber-Attack Against Ukrainian Critical Infrastructure[END_REF]. The common feature of the systems above is that they are all safety critical and failures may cause catastrophic consequences. Thus, the concern for consequences at the physical level puts CPS security apart from standard IT security, and demands for ad hoc solutions to properly address such novel research challenges.

The physical plant of a CPS is often represented by means of a discrete-time state-space model 3 consisting of two difference equations of the form

x k+1 = Ax k + Bu k + w k y k = Cx k + e k
where x k ∈ R n is the current (physical) state, u k ∈ R m is the input (i.e., the control actions implemented through actuators), w k ∈ R n is the system uncertainty, y k ∈ R p is the output (i.e., the measurements from the sensors), and e k ∈ R p is the measurement error. A, B, and C are matrices modelling the dynamics of the physical system. Cyber-physical attacks typically tamper with both the physical (sensors and actuators) and the cyber layer. In particular, cyber-physical attacks may affect directly the sensor measurements or the controller commands (see Figure 1):

-Attacks on sensors consist of reading and possibly replacing the genuine sensor measurements y k with fake measurements y a k . -Attacks on actuators consist of reading, dropping and possibly replacing the genuine controller commands u k with malicious commands u a k , affecting directly the actions the actuators may execute. One of the central problem in the safety verification of CPSs is the reachability problem: can an unsafe state be reached by an execution of the system (possibly under attack) starting from a given initial state? In general, the reachability problem for hybrid systems (and hence CPSs) is stubbornly undecidable, although boundaries of decidability have been extensively explored in the past couple of decades [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Henzinger | What's decidable about hybrid automata[END_REF][START_REF] Lafferriere | O-minimal hybrid systems[END_REF][START_REF] Vladimerou | STORMED hybrid systems[END_REF][START_REF] Roohi | Remedies for building reliable cyber-physical systems[END_REF]. Thus, despite the undecidability of the safety problem, a number of formal verification tools for hybrid systems have been recently proposed, based on approximation techniques to obtain an estimation of the set of reachable states: SpaceEx [START_REF] Frehse | SpaceEx: Scalable Verification of Hybrid Systems[END_REF], PHAVer [START_REF] Frehse | Phaver: Algorithmic verification of hybrid systems past hytech[END_REF] and SpaceEx AGAR [START_REF] Bogomolov | Assume-Guarantee Abstraction Refinement Meets Hybrid Systems[END_REF], for linear/affine dynamics, and HSolver [START_REF] Ratschan | Safety verification of hybrid systems by constraint propagationbased abstraction refinement[END_REF], C2E2 [START_REF] Duggirala | C2E2: A Verification Tool for Stateflow Models[END_REF] and FLOW * [START_REF] Chen | Flow*: An Analyzer for Non-linear Hybrid Systems[END_REF], for non-linear dynamics. Among these, the hybrid solver PHAVer addresses the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives, so-called rectangular hybrid automata [START_REF] Henzinger | What's decidable about hybrid automata[END_REF]. Affine dynamics are handled by on-the-fly overapproximation and partitioning of the state space based on user-provided constraints and the dynamics of the system. To force termination and manage the complexity of the computations, methods to conservatively limit the number of bits and constraints are adopted.

Contribution. We implement in the MODEST TOOLSET [START_REF] Hartmanns | The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification[END_REF], an integrated collection of tools for the design and the formal analysis of stochastic hybrid automata, a simple but totally realistic and nuanced cyber-physical system. The example has been proposed by Lanotte et al. [START_REF] Lanotte | A Formal Approach to Cyber-Physical Attacks[END_REF] to highlight different classes of attacks on sensors and actuators, in a way that is basically independent on the size of the system. Our case study is implemented in the main modelling language HMODEST [START_REF] Hahn | A compositional modelling and analysis framework for stochastic hybrid systems[END_REF], a process-algebra based language that has an expressive programming language-like syntax to design complex systems.

The current version of the toolset comprises several analysis backends, in particular it provides a safety model checker, called prohver, that relies on a modified version of the hybrid solver PHAVer [START_REF] Frehse | Phaver: Algorithmic verification of hybrid systems past hytech[END_REF]. We use prohver to analyse three simple but significative cyber-physical attacks targeting sensors and/or actuators of our case study by compromising either the corresponding physical device or the communication network used by the device. The three attacks have already been carefully studied in [START_REF] Lanotte | A Formal Approach to Cyber-Physical Attacks[END_REF] focussing on the time aspects of the attacks (begin, duration, etc.) and the physical impact on the system under attack (deadlock, unsafe behaviour, etc.). Here, we test the safety model checker prohver as an automatic tool to get the same (or part of the) results that have been manually proved in [START_REF] Lanotte | A Formal Approach to Cyber-Physical Attacks[END_REF]. We then compare its effectiveness in verifying CPS security properties, when compared to other state-of-the-art models checkers, such as PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF], UPPAAL [START_REF] Behrmann | UPPAAL 4.0[END_REF] and Real-Time Maude [START_REF] Ölveczky | Semantics and pragmatics of Real-Time Maude[END_REF].

Outline. In Section 2 we give a brief description of the MODEST TOOLSET. In Sections 3 and 4 we first describe and then implement in HMODEST our case study. In Section 5 we put under stress the safety model checker prohver for a security analysis of our case study under three different cyber-physical attacks. In Section 6 we draw conclusions, compare the expressivity of the MODEST TOOLSET with respect to other model-checkers, and discuss related work in the context of formal methods for CPS security.

The MODEST TOOLSET

The MODEST TOOLSET [START_REF] Bohnenkamp | motor: The modestTool environment[END_REF] has been originally proposed as an integrated collection of tools for the design and the formal analysis of stochastic timed automata (STA). More recently, it has been extended to add differential equations and inclusions as an expressive way to model continuous system evolutions [START_REF] Hahn | A compositional modelling and analysis framework for stochastic hybrid systems[END_REF]. Thus, the current version of the toolset [START_REF] Hartmanns | The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification[END_REF] is now based on the rich semantic foundation of networks of stochastic hybrid automata (SHA), i.e., sets of automata that run asynchronously and can communicate via shared actions and global variables.

SHA combine three key modelling concepts:

-Continuous dynamics to represent continuous processes, such as physical laws or chemical reactions, the evolution of general continuous variables over time can be described using differential (in)equations. -Nondeterminism to model concurrency (via an interleaving semantics) or the absence of knowledge over some choice, to abstract from details, or to represent the influence of an unknown environment. -Probability to model situations in which an outcome is uncertain but the probabilities of the outcomes are known; these choices may be discrete ("probabilistic") or continuous ("stochastic").

The current version of the MODEST TOOLSET comprises analysis backends for model checking timed automata (mctau) and probabilistic timed automata (mcpta), and for statistical model checking of stochastic timed automata (modes). However, in this paper we focus on the safety model checker for SHA, called prohver, that relies on a modified version of the hybrid solver PHAVer [START_REF] Frehse | Phaver: Algorithmic verification of hybrid systems past hytech[END_REF].

The main modelling language is HMODEST [START_REF] Hahn | A compositional modelling and analysis framework for stochastic hybrid systems[END_REF], a process-algebra based language that has an expressive programming language-like syntax to design complex models in a reasonably concise manner. Here, we provide a brief and intuitive explanation of the main constructs.

A HMODEST specification consists of a sequence of declarations (constants, variables, actions, and sub-processes) and a main process behaviour. The most simple process behaviour is expressed by (prefixing) actions that may be used for synchronising parallel components. The construct do serves to model loops, i.e., unguarded iterations that can be exited via the special action break. There is a construct par to launch two or more processes in parallel, according to an interleaving semantics. The construct alt models nondeterministic choice. The invariant construct serves to control the evolution of continuous variables. Furthermore, all constructs can be decorated with guards, to represent enabling conditions, by means of the when construct. We can use both invariant and when constructs to specify that a behaviour should be executed after a precise amount of time. Thus, we can write invariant(c ≤ k) when (c ≥ k) P(), where c is a clock variable and k a real value, to model that the process P() may start is execution only after k time units; if k = 0 then the execution of P() may start immediately.

In order to better explain these constructs, we model a small example described by means of a standard timed process-calculus notation (say, Hennessy and Regan's TPL [START_REF] Hennessy | A process algebra for timed systems[END_REF]). Consider a Master and a Slave process that may synchronise via a private synchronisation channel sync, and use a private channel ins to allow the Master to send instructions to the Slave. Depending on the received instructions, the Slave either synchronises with the Master and then restart, or sleeps for one time unit and then ends its execution. Once synchronised, the Master sleeps for two time units. Formally, Figure 2 shows an implementation in HMODEST of the system above. Both master and slave declare private clocks that are reset each time is necessary to impose a specific time delay. Value-passing communication is implemented via the two actions go and end ; the testing via nondeterministic choice.

Besides these operators, the case study that we will present in the next section includes specifications over continuous variables, such as constraints over the derivate of continuous variables of the form a ≤ ẋ ≤ b, with a and b constant (as in rectangular hybrid automata), or nondeterministic initialisations of the form z ∈ [a, b]. The former requirement is realised in HMODEST by means of an invariant construct: invariant(der (x ≥ a) && der (x ≤ b)). The latter constraint is implemented via the any construct. For instance, any(z, z >= a && z <= b) returns a value nondeterministically chosen in the real interval [a, b].

The safety model checker prohver allows the verification of reachability properties of the form P max(♦ time≤T e). This query returns un upper bound of the probability of reaching the states characterised by the deterministic expression e within the time bound T . 4 Moreover, as the models may be nondeterministic, P max() computes the probability over all possible resolutions of nondeterminism.

A case study

In this section, we describe the case study recently introduced in [START_REF] Lanotte | A Formal Approach to Cyber-Physical Attacks[END_REF]. Here, we wish to remark that while the example is quite simple, it is actually far from trivial and designed to describe a wide number of attacks. Furthermore, for simplicity, in the description of the case study we use a discrete-time model, although in its implementation we will adopt a continuous notion of time.

Consider a CPS Sys in which the temperature of an engine is maintained within a certain range by means of a cooling system controlled by a controller.

The system is also equipped with a IDS that does runtime safety verification. Let's describe both the physical and the cyber component of the CPS Sys.

The physical environment of Sys is constituted by: a variable temp, initialised to 0, for the current temperature of the engine; a sensor sens measuring the temperature of the engine; an actuator cool to turn on/off the cooling system; cool ranges over the set {-1, +1} to denote active and inactive cooling, respectively; the evolution equation temp k+1 = temp k +cool k +w k , where

w k ∈ [-0.4, +0.4]
denotes the uncertainty associated to temp; thus the variable temp is increased (resp., is decreased) of one degree per time unit if the cooling system is inactive (resp., active) up to a bounded uncertainty w k ; a measurement equation sens k = temp k + e k , where e k ∈ [-0.1, +0.1] denotes the noise associated to the sensor sens; an invariant function returning the Boolean true if the state variable temp lays in the interval [0, 20], false otherwise; a safety function returning the Boolean true if the safety conditions are satisfied, false otherwise; the safety of the CPS depends on a (fictitious) variable stress keeping track of the level of stress of the mechanical parts of the engine due to high temperatures; stress ranges over the set {0, 1, 2, 3, 4, 5}, where 0 means no stress and 5 high stress; formally, stress k+1 = min(5, stress k + 1) if temp k > 9.9, while stress k+1 = 0 if temp k ≤ 9.9.

Let us define the cyber component of the CPS Sys. For simplicity, we use a simple process-calculus notation similar to that of Lanotte and Merro's CaIT [START_REF] Lanotte | A semantic theory of the Internet of Things[END_REF]. The logics of Sys is modelled by means of two parallel processes: Ctrl and IDS . The former models the controller activity, consisting in reading the temperature of the engine and in governing the cooling system; whereas the latter models a simple intrusion detection system that attempts to detect and signal abnormal behaviours of the system. Intuitively, Ctrl senses the temperature of the engine via the sensor sens (reads the sensor) at each time slot. When the sensed temperature is above 10 degrees, the controller activates the coolant via the actuator cool (sending a command to the actuator). The cooling activity is maintained for 5 consecutive time units. After that time, the controller synchronises with the IDS component via a synchronisation channel sync, and then waits for instructions, via a value-passing channel ins. The IDS component checks whether the sensed temperature is still above 10. If this is the case, it sends an alarm of "high temperature", via a specific channel, and then says to Ctrl to keep cooling for a further 5 time units; otherwise, if the temperature is not above 10, the IDS component requires Ctrl to stop the cooling activity. More formally, The whole cyber component of Sys is given by the parallel composition of the two processes Ctrl and IDS in which the channels sync and ins have been restricted: (Ctrl IDS )\{sync, ins}.

Ctrl = read sens(x).if (x >
In Figure 3, the left graphic collect a campaign of 100 simulations of our engine in MATLAB, lasting 250 time units each, showing that the value of the state variable temp when the cooling system is turned on (resp., off) lays in the interval (9.9, 11.5] (resp., (2.9, 8.5]); these bounds are represented by the dashed horizontal lines. The right graphic of the same figure shows three possible evolutions in time of the state variable temp: (i) the first one (in red), in which the temperature of the engine always grows as slow as possible and decreases as fast as possible; (ii) the second one (in blue), in which the temperature always grows as fast as possible and decreases as slow as possible; (iii) and a third one (in yellow), in which, depending whether the cooling is off or on, temperature grows or decreases of an arbitrary offset laying in the interval [0.6, 1.4].

An implementation in HMODEST

In this section, we provide our implementation in HMODEST of the case study presented in the previous section. The whole system is divided in three high level processes running in parallel (see Figure 4):

-Plant(), modelling the physical aspects of the system; -Logics(), describing the logical (or cyber) component of a CPS; -Network(), representing the network connecting Plant() and Logics().

The process Plant() consists of the parallel composition of four processes: Engine(), Actuators(), Sensors() and Safety() (see Figure 5). The former models the dynamics of the variable temp depending on the cooling activity. The temperature evolves in a continuous manner, and its rate is described by means of differential inclusions of the form a ≤ ẋ ≤ b implemented via the construct invariant. The on action triggers the coolant and drives the process Engine() into a state CoolOn() in which the temperature decreases at a rate comprised in the range The second parallel component of Plant() is the process Sensors() that receives the requests to read the temperature, originating from the Logics(), and serves them according to the measurement equation seen in the previous section. This is modelled by updating the variable sens with an arbitrary real value laying in the interval [temp -NOISE, temp + NOISE].

The process Actuators() relays the commands of the controller Ctrl() to the Engine() to turn on/off the cooling system.

The last parallel component of the process Plant() is the process Safety(). This process defines a local variable stress depending on the temperature reached by the engine; we recall that stress = 0 denotes no stress while stress = 5 represents maximum stress. Here, is worth mentioning that the variable stress could be implemented either as a bounded integer variable, which would increase the discrete complexity of the underlying hybrid automaton, or as a continuous variable with dynamics set to zero (i.e., der(stress) = 0) that would increase the continuous complexity of the automaton. We have adopted the second option as it ensures better performances. The Safety() process sets the global Boolean variable safe to false only when the system reaches the maximum stress, i.e., stress = 5, and reset it to true otherwise. Thus, this variable says when the CPS is currently in a state that is violating the safety conditions. Similarly, the global Boolean variable is deadlock is set to true whenever the system invariant is violated; in that case the whole CPS stops. The process Logics() consists of the parallel composition of two processes: Ctrl() and IDS() (see Figure 6). The former senses the temperature by triggering a read sensor ctrl action to request a measurement and waits for an ack sensor ctrl action to read the measurement in the variable sens. Depending on the value of sens the controller decides whether to activate or not the cooling system. If sens ≤ 10 the process sleeps for one time unit and then check the temperature again. If sens > 10 then the controller activates the coolant by emitting the set cool on action that will reach the Engine() (via the Network()'s proxy). Afterwards the control passes to the process Check() that verifies whether the current cooling activity is effective in dropping the temperature below 10. The process Check() maintains the cooling activity for 5 consecutive time units. After that, it synchronises with the process IDS() via the action sync ids, and waits for instructions from IDS(): (i) keep cooling for other 5 time units and then check again, or (ii) stop the cooling activity and returns. These two instructions are represented by means of the actions keep cooling and stop cooling, respectively.

The second component of the process Logics() is the process IDS(). The IDS() process waits for the synchronisation action sync ids from Check(). Then, it triggers the action read sensor ids to request a measurement and waits for the ack sensor ids action to read the measurement. If sens ≤ 10 it signals to Ctrl() to stop cooling (via the action), otherwise, if sens > 10, it signals to keep cooling and fires an alarm by setting a global Boolean variable alarm to true (for verification reasons we immediately reset this variable to false).

The process Network() consists of the parallel composition of two processes: Proxy actuator() and Proxy sensor() (see Figure 7). The former provides the remote actuation. Basically, it forwards the actuators commands originating from the process Ctrl() to the process Actuators(). The process Proxy sensor() waits for requests of measurement originating from processes Ctrl() or IDS() (we use different actions for each of them) and relay these requests to the process Sensor() that implements the measurement equation. When the temperature has been detected an ack signal is returned and propagated up to the requesting process.

Verification. We conduct our safety verification using 4 notebooks with the following set-up: (i) 2.8 GHz Intel i7 7700 HQ, with 16 GB memory, and Linux Ubuntu 16.04 operating system; (ii) MODEST TOOLSET Build 3.0.23 (2018-01-19).

In order to assess the correct functioning of our implementation, we verify a number of properties of our CPS Sys by means of the safety model checker prohver. Here, it is important to recall that prohver relies on the hybrid solver PHAVer which computes an overapproximation of the reachable states to ensure termination and accelerate convergence [START_REF] Frehse | Phaver: Algorithmic verification of hybrid systems past hytech[END_REF]. As consequence, the probability returned by the verification of a generic property Pmax (♦ T e prop ) is an upper bound of the exact probability, and hence it is significant only when equal to zero (i.e., when the property is not satisfied). However, as our CPS Sys presents a linear dynamics it is possible to compute the exact probability by launching our analyses with the NO CHEAP CONTAIN RETURN OTHERS flag (see [START_REF] Frehse | Phaver language overview v0[END_REF]) which enables the exact computation of the reachable sets, with obvious implications on the time required to complete the analyses. As our case study does not present a probabilistic behaviour, the results of our analyses will always range in the set {0, 1} (unsatisfied/satisfied) with a 100% accuracy.

Furthermore, as a formula e is satisfied if and only if ♦¬e is unsatisfied, we can use prohver to verify properties expressed in terms of time bounded LTL formulae of the form [0,T ] e prop or ♦ [0,T ] e prop . Actually, in our analyses we will always verify properties of the form [0,T ] e prop , relying on the quicker overapproximation when proving that the property is satisfied, and resorting to the slower exact computation when proving that the property is not satisfied.

Thus, we have formally proved that in all possible executions that are (at most) 100 time instants long the temperature of the system Sys oscillates in the real interval [2.9, 11.5] (after a short initial transitory phase):

[0,100] (global clock ≥ 5 =⇒ (temp ≥ 2.9 ∧ temp ≤ 11.5)) .

More generally, our implementation of Sys satisfies the following three properties:

-[0,100] (¬deadlock), saying that the system does not deadlock; -[0,100] (saf e), saying that the system does not violate the safety conditions; -[0,100] (¬alarm): saying that the IDS does not fire any alarm. The verification of these three properties requires around 15 minutes each, thanks to the underlying overapproximation.

In the next section, we will verify our CPS in the presence of three different cyber-physical attacks targeting either the sensor sens or the actuator cool . The reader can consult our models at http://profs.scienze.univr.it/∼merro/MODEST-FORTE/.

A Static Security Analysis

In this section, we use the safety model checker prohver to test its limits when doing static security analysis of CPSs. In particular, we implement three simple cyber-physical attacks targeting our system Sys:

a DoS attack on the actuation mechanism that may push the system to violate the safety conditions and hence in the invariant conditions; a DoS attack on the sensor that may deadlock the CPS without being noticed by the IDS; an integrity attack on the sensor, again undetected by the IDS , that may drive the CPS into into a unsafe state but only for a limited period of time.

These attacks are implemented by tampering with either the physical devices (actuators and/or sensors) or the communication network (man-in-the-middle). In order to implement an attack on the sensor (resp., actuator) we suppose the attacker is able to compromise the Sensors() (resp., Actuators()) process. Whereas the attacks targeting the communication network compromise either the Proxy sensor() or the Proxy actuator() process, depending whether they are targeting the sensor or the actuator. In general, attacks on the communication network do not require a deep knowledge on the physical dynamics of the CPS.

Attack 1. The first attack targets the actuator cool in a very simple manner. It operates exclusively in a specific time instant m, when it tries to drop the command to turn on the cooling system coming from the controller. Figure 8 shows the implementation of this man-in-the-middle attack compromising the Proxy actuator() process.

We recall that the controller will turn on the cooling system only if it senses a temperature above 10 (as NOISE = 0.1, this means temp > 9.9). It is not difficult to see that this may happen only if m > 7 (in the time instant 7 the maximum temperature that may be reached by the engine is 7•(DT+UNCERT) = 7 • (1 + 0.4) = 9.8 degrees). Since the process Ctrl() never re-send commands to the actuator, if the attacker is successful in dropping the command to turn on the cooling system in the time slot m then the temperature will continue to rise, and after 2 time instants, in the time instant m + 2, the system will violate the safety conditions. This is noticed by the IDS() that will fire alarms every 5 time instants, until the CPS deadlocks because temp > 20.

We have verified the same properties stated in the previous section for the system Sys in isolation. None of those properties holds when the attack above operates in an instant m > 7. In particular, for m > 7 the system becomes unsafe in the time instant m + 2, and the IDS() detects the violation of the safety conditions with a delay of only 2 time instants. Summarising:

Attack 1: tested properties m ≤ 7 m > 7 [0,100] (¬deadlock) [0,100] (saf e) [0,100] (¬alarm) [0,m+1] (saf e) [0,m+2] (saf e) [0,m+3] (¬alarm) [0,m+4] (¬alarm)
The properties above have been proved for all discrete time instants m, with 0 ≤ m ≤ 96. The longest among these analyses required 20 minutes when overapproximating and at most 7 hours when doing exact verification.

Attack 2. The second attack compromises the sensor in order to provide fake measurements to the controller. The compromised sensor operates as follows: (i) in any time instant smaller than or equal to 1 the sensor works correctly, (ii) in any time instant greater than 1 the sensor returns the temperature sensed at time 1. Figure 9 provides an implementation of the compromised sensor. In the presence of this attack, the process Ctrl() will always detect a temperature below 10 and never activate the cooling system or the IDS. The system under attack will move to an unsafe state until the system invariant will be violated and the system will deadlock. Indeed, in the worst case scenario, after 9.9 DT+UNCERT = 9.9 1.4 = 8 time instants the value of temp will be above 9.9 degrees, and after further 4 time instants the system will violate the safety conditions. Furthermore, in the time instant = 20 1.4 = 15 the invariant may be broken and the system may deadlock because the state variable temp reaches 20.4 degrees. This is a lethal attack as it causes a deadlock of the system. It is also a stealthy attack as it remains unnoticed until the end.

The results of our security analysis are summarised in the following table: The longest among these analyses required 35 minutes when overapproximating and at most 5 hours when doing exact verification. Please, notice that this attack does not require any specific knowledge of the sensor device (such as the measurement equation). Thus, the same goal could be obtained by means of a man-in-the-middle attack that compromises the Proxy sensor() process.

Attack 3. Our last attack is a variant of the previous one as it provides the controller with a temperature decreased by an offset (in this case 2), for n consecutive time instants. Unlike the previous attack, in case of encrypted communication, this attack cannot be mounted in the network as it requires the knowledge of the measurement equation. The effects of this attack on the system depends on its duration n.

-For n ≤ 7 the attack is harmless as the variable temp may not reach a (critical) temperature above 9.9; thus, all properties seen for the system in isolation remain valid when the system is under attack. -For n = 8, the variable temp might reach a temperature above 9.9 and the attack would delay the activation of the cooling system of one time instant. As a consequence, the system might get into an unsafe state in the time instants 12 and 13, but no alarm will be fired (stealthy attack ). This is proved by verifying the following properties: The properties above have been proved for all discrete time instants n, with 0 ≤ n ≤ 85. The longest among these analyses required 1 hour when overapproximating and at most 7 hours when doing exact verification.

Conclusions

As said in the Introduction, the safety model checker within the MODEST TOOLSET relies on a modified version of the hybrid solver PHAVer, whose specification language is a slight variation of hybrid automata supporting compositional reasonings, where input and output variables are clearly distinguished [START_REF] Lynch | Hybrid I/O automata[END_REF]. Although, PHAVer would be a good candidate for the verification of small CPSs, we preferred to specify our case study in the high-level language HMODEST, supporting: (i) differential inclusion to model linear CPSs with constant bounded derivatives; (ii) linear formulae to express nondeterministic assignments within a dense interval; (iii) compositional programming style inherited from process algebra (e.g., parallel composition, nondeterministic choice, loops, etc.); (iv) shared actions to synchronise parallel components.

In HMODEST, we have implemented a simple but totally realistic and nuanced cyber-physical system together with three cyber-physical attacks targeting the sensor or the actuator of the system. In particular, we have proposed: (i) a DoS attack on the actuator that operates as a man-in-the-middle on the connecting network; (ii) a DoS attack on the sensor that is achieved by compromising the sensor device; (iii) an integrity attack on the sensor, again by compromising the sensor device. Our implementation is quite clean and concise, although the current version of the language has still some problems in representing both instantaneous and delayed behaviours in an effective manner (we did not use the elegant delay() construct as each instance introduces a new clock, with heavy implications on the verification performance). Furthermore, in order to verify our safety and invariant conditions we have implemented a Safety() process that is not really part of our CPS. From a designer point of view it would have been much more practical to use some kind of logic formula, such as: ∃♦( [t,t+5] temp > 9.9).

For the security analysis we have used the safety model checker prohver. Basically, we have verified LTL properties on the system under attack. Although, we have verified most of the properties that have been manually proved in [START_REF] Lanotte | A Formal Approach to Cyber-Physical Attacks[END_REF], we have not been able to capture time properties on the responsiveness of the IDS to violations of the safety conditions. Properties such as:

there are integers m and k such that the system may have an unsafe state at some instant n > m, and the IDS detects this violation with a delay of at least k time instants (k being a lower bound of the reaction time of the IDS); there is an instant n where the IDS fires an alarm but neither an unsafe state nor a deadlock occurs between the instants n -k and n + k: this would provide a tolerance of the occurrence of false positive.

Note that prohver has been designed to do probabilistic model-checking, while in this paper we only do model checking. Actually, one of the reasons why we implemented our case study in HMODEST is because we aim at strengthening our security analysis by resorting to probabilistic model checking. This would allow us to replace nondeterministic uncertainty and nodeterministic noise with probability distributions (for instance, normal distributions are very common in this context).

A comparison with other model-checkers. We tried to verify our case study also with other model-checkers for distributed systems providing high-level specification languages and expressive query languages, such as PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF], UPPAAL [START_REF] Behrmann | UPPAAL 4.0[END_REF] and Real-Time Maude [START_REF] Ölveczky | Semantics and pragmatics of Real-Time Maude[END_REF]. In particular, as our example has a discrete notion of time we started looking at verification tools supporting discrete time.

PRISM, for instance, relies on Markov decision processes or discrete-time Markov chains, depending whether one is interested in modelling nondeterminism or not. It supports the verification of both CTL and LTL properties (when dealing with nonprobabilistic systems). This allowed us to express the formula ∃♦( [t,t+5] temp > 9.9) to verify violations of the safety conditions, avoiding the implementation of the Safety() process. However, using integer variables to represent state variables with a fixed precision requires the introduction of extra transitions (to deal with nondeterministic errors) that significantly complicates the PRISM model.

In this respect, UPPAAL appears to be more efficient than PRISM, as we have been able to concisely express the error occurring in integer state variables thanks to the select() construct, in which the user can fix the granularity adopted to approximate a dense interval. This discrete representation provides an underapproximation of the system behaviour; thus, a finer granularity translates into an exponential increase of the complexity of the system, with obvious consequences on the verification performance. UPPAAL has provided us with a simple way to implement the preemptive power of cyber-physical attacks by assigning priorities to processes. Thus, a system under attack can be easily represented by simply putting in parallel the system and the attacker. The tool supports the verification of a simplified version of CTL properties (no nesting of path formulae is allowed). Thus, as in HMODEST, we cannot express the formula ∃♦( [t,t+5] temp > 9.9) and we had to implement a Safety() process.

Finally, we tried to model our case study in Real-Time Maude, a completely different framework for real-time systems, based on rewriting logic. The language supports object-like inheritance features that are quite helpful to represent complex systems in a modular manner. Communication channels have been used to implement our attacks on the physical devices. Furthermore, we used rational variables for a more concise discrete representation of state variables. We have been able to verify LTL and T-CTL properties, although the verification process resulted to be very slow due to a proliferation of rewriting rules when fixing a reasonable granularity to approximate dense intervals. As the verification logic is quite powerful, there is no need to implement the Safety() process.

Formal methods for CPS security. A few works use formal methods for CPS security, although they apply methods, and most of the time have goals, that are quite different from ours. As already said, the case study has been taken from [START_REF] Lanotte | A Formal Approach to Cyber-Physical Attacks[END_REF]. In that paper the authors present a threat model for a formal study of a variety of cyber-physical attacks. They also propose a formal technique to assess the tolerance of CPSs to classes of attacks. The paper provides a stepping stone for formal and automated analysis techniques for checking the security of CPSs.

In [START_REF] Vigo | The Cyber-Physical Attacker[END_REF][START_REF] Vigo | Availability by Design: A Complementary Approach to Denial-of-Service[END_REF], Vigo presents an attack scenario that addresses some of the peculiarities of a cyber-physical adversary, and discussed how this scenario relates to other attack models popular in the security protocol literature. Unlike us, this paper focuses on DoS attacks without taking into consideration timing aspects. Rocchetto and Tippenhaur [START_REF] Rocchetto | On Attacker Models and Profiles for Cyber-Physical Systems[END_REF] introduce a taxonomy of the diverse attacker models proposed for CPS security and outline requirements for generalised attacker models; in [START_REF] Rocchetto | CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions[END_REF], they then propose an extended Dolev-Yao attacker model suitable for CPS security. In their approach, physical layer interactions are modelled as abstract interactions between logical components to support reasoning on the physical-layer security of CPSs. This is done by introducing additional orthogonal channels. Time is not represented. Nigam et al. [START_REF] Nigam | Towards the Automated Verification of Cyber-Physical Security Protocols: Bounding the Number of Timed Intruders[END_REF] work around the notion of Timed Dolev-Yao Intruder Models for Cyber-Physical Security Protocols by bounding the number of intruders required for the automated verification of such protocols. Following a tradition in security protocol analysis, they provide an answer to the question: How many intruders are enough for verification and where should they be placed? They also extend the strand space model to CPS protocols by allowing for the symbolic representation of time, so that they can use Real-Time Maude [START_REF] Ölveczky | Semantics and pragmatics of Real-Time Maude[END_REF] along with SMT support. Their notion of time is however different from ours, as they focus on the time a message needs to travel from an agent to another. The paper does not mention physical devices, such as sensors and/or actuators.

Fig. 1 .

 1 Fig. 1. A threat model for CPSs

=Fig. 2 .

 2 Fig. 2. Master and Slave processes in HMODEST

Fig. 3 .

 3 Fig. 3. Simulations in MATLAB of Sys

/Fig. 4 .

 4 Fig. 4. Implementation in HMODEST of Sys

Fig. 5 .

 5 Fig. 5. Plant() sub-processes

}Fig. 6 .

 6 Fig. 6. Logics() sub-processes

Fig. 7 .

 7 Fig. 7. Network() process

}Fig. 8 .

 8 Fig. 8. DoS attack to the actuator

Fig. 9 .

 9 Fig. 9. DoS attack to the sensor

Attack 2 :

 2 tested properties [0,100] (¬alarm) [0,100] (saf e) [0,100] (¬deadlock) [0,11] (saf e) [0,12] (saf e) [0,14] (¬deadlock) [0,15] (¬deadlock)

Figure 10 Fig. 10 .

 1010 Fig. 10. Integrity attack to the sensor device

  10) {Cooling} else {sleep.Ctrl } Cooling = write cool on .sleep(5).Check Check = sync.ins(y).if (y = keep cooling) {sleep(5).Check } else {write cool off .sleep.Ctrl } IDS = sync.read sens(x).if (x > 10) ins keep cooling .{alarm high temp .sleep.IDS } else {ins stop .sleep.IDS }

	actual temperature (deg)
	0	20	40	60	80	100
			experiments

  • [0,100] ((global clock < 12 ∨ global clock > 14) =⇒ saf e) • [0,100] ((global clock ≤ 12 ∧ global clock ≥ 12) =⇒ saf e) • [0,100] ((global clock ≤ 13 ∧ global clock ≥ 13) =⇒ saf e) • [0,100] (¬alarm) .-For n > 8 the system may get into an unsafe state in a time instant between 12 and n + 12. The IDS will fire the alarm but it will definitely miss a number of violations of safety conditions as after the instant n + 6 it does not fire any alarm, although we prove there are unsafe states. This is a temporary attack as the system behaves correctly after the time instant n + 12. Summarising:• [0,100] (¬deadlock) • [0,100] ((global clock < 12 ∨ global clock > n + 12) =⇒ saf e) • [0,100] ((global clock ≥ 12 ∧ global clock ≤ n + 12) =⇒ saf e) • [0,100] ((global clock > n + 6 ∧ global clock ≤ n + 12) =⇒ saf e) • [0,100] ((global clock < n+1 ∨ global clock > n + 6) =⇒ ¬alarm) • [0,100] ((global clock ≥ n+1 ∧ global clock ≤ n + 6) =⇒ ¬alarm) .

Later in the paper, we will show how to get the exact probability.

Acknowledgements. We thank the anonymous reviewers for their insightful and careful reviews that allowed us to significantly improve the paper. We thank Fabio Mogavero for stimulating discussions on model checking tools, and Arnd Hartmanns for "tips and tricks" on the MODEST TOOLSET. This work has been partially supported by the project "Dipartimenti di Eccellenza 2018-2022" funded by the Italian Ministry of Education, Universities and Research (MIUR).


Doctorat De L'université

D E Lyon

L ' Université

Lumière Lyon

Tatiana Martinez Zavala

Rémi Bazillier

Jean-Paul Azam

N° d'ordre NNT : 2017LYSE2150

diffusion

Ce document est diffusé sous le contrat

Essays on Mexican Migration to the US

Tatiana Martinez Zavala

Introduction Général

L'introduction général a abordé plusieurs sujets qui ont façonné la migration mexicaine vers les États-Unis d'aujourd'hui. D'un point de vue historique, nous avons suggéré des déterminants précoces du phénomène, qui ont eu un impact sur les modèles de migration actuels grâce aux réseaux sociaux.

Bien qu'un ensemble diversifié d'estimations aient été élaborées pour tenir compte à la fois des populations d'immigrants légaux et illégaux aux États-Unis, il y a encore des incertitudes quant aux chiffres réels. Cependant, les Mexicains aux États-Unis représentent la part la plus importante de la population non autorisée et environ un tiers de la population totale née à l'étranger. Cette grande quantité d'immigrants mexicains a donné des lois et des politiques de plus en plus restrictives, aboutissant à la proposition controversée de Trump de construire un mur le long de la frontière entre les États-Unis et le Mexique. Ainsi, bien que la migration puisse aider les familles migrantes à résister à une pauvreté à court terme, il semble y avoir un effet préjudiciable à long terme en ce qui concerne la mobilité sociale, mesurée par l'éducation.

Mots clés : Mobilité sociale, Education, Migration internationale.

JEL Classification I21, J61, J62.

  migration illégale et criminalité organisée Cet article ajoute une nouvel aspect aux résultats trouvés dans le premier chapitre. L'article fournit un cadre simple reliant le crime organisé, l'aide étrangère et l'immigration clandestine. À notre connaissance, c'est la première tentative d'analyse de cette relation tripartite dans la littérature. Nous fournissons également un soutien empirique pour l'hypothèse et les résultats de notre modèle avec des données de plusieurs pays, étant donné que l'analyse d'un point de vue exclusivement du Mexique est impossible sans des données désagrégées. Grâce à un cadre théorique simple, nous avons modelé une population de migrants potentiels qui observent les niveaux de développement, le contrôle des frontières et le crime organisé dans leur pays, puis migrent si leur utilité attendue est supérieure à celle de rester chez eux. L'hétérogénéité des individus permet établir un individu marginal qui aide à mesurer la proportion de migrants. Le modèle nous permetre observer que cette proportion de migrants diminue si les résultats du développement s'améliorent ou si plus de gardes-frontières ou de crime organisé sont observés. Le gouvernement domestique dépense dans le développement pour limiter les flux migratoires, mais compte tenu que d'autres variables diminuent la migration, elle peut dévier certaines ressources pour les projets . Étant donné que la réduction du crime organisé par l'aide internationale au développement aura un impact positif sur les migrations, le pays étranger opte pour une politique de contrôle des frontières plus forte et un niveau d'aide plus faible, ce qui se traduit par une criminalité organisée supérieure à l'optimum. Nous fournissons une stratégie empirique pour tester l'hypothèse et les résultats de notre modèle à travers d'un modèle d'équation simultané utilisant des données de plusieurs pays maillés : d'un coté, des pays qui recoivent l'aide internationale et envoient des migrants, et des l'autre des pays qui accueillent des migrants et donne de l'aide internationale au équation de gravité de migration et une équation d'aide international au développement. La plupart de nos résultats empiriques correspondent à notre modèle, ce qui suggère un effet positif de l'aide aux migrations, un effet négatif de la criminalité organisée sur les migrations et, surtout, la criminalité organisée et les flux migratoires élevés entraînent une aide plus faible. Par conséquent, nous sommes en mesure d'appuyer la constatation de notre modèle théorique selon laquelle le donateur permet un niveau supérieur de criminalité organisée dans le pays qui envoie des migrants comme autre moyen de réduire les flux migratoires. Mots clés : Migration illégale ; L'aide internationale ; Développement ; Crime organisé. JEL Classification : F22, F35.Chapitre 3La chute de la mobilité lors du déplacement : une étude sur la mobilité sociale des migrants mexicains vers les États-Unis Bien que les chapitres précédents se concentrent sur les déterminants de la migration, ce chapitre vise à étudier l'impact de la migration parentale sur leurs enfants. Concrêtement , L'objectif de cet article est de contribuer à la migration et à la mobilité sociale en fournissant des estimations de l'impact causal de la migration sur la mobilité éducative. Bien que la plupart de cette littérature se concentre sur la population immigrante, nous nous concentrons ici sur l'effet de la migration sur la famille des migrants, une approche qui n'a pas été précédemment suivie au mieux de nos connaissances.Nous utilisons une stratégie de variables instrumentales qui exploite les données historiques sur les migrations et les réseaux ferroviaires des années 1920 au Mexique. Bien que de nombreuses études migratoires mexicaines aient utilisé ces variables, nous fournissons des preuves supplémentaires de la validité des instruments, d'autant plus que notre échantillon de parents est partiellement contemporain des données historiques.Nos résultats suggèrent un effet pertinent de la migration sur la mobilité sociale, ce qui augmente les coefficients de corrélation à plus de deux fois par rapport à celui d'un cadre OLS simple. Cela signifie que les enfants des migrants sont nettement moins mobiles que ceux des parents non migrants. En outre, le fait que notre terme d'interaction soit positif suggère également que les parents ayant des diplômes supérieures diminuent considérablement les effets négatifs de la migration sur le niveau de scolarité.Nous fournissons des explications possibles de nos résultats et suggérons que la mobilité éducative des migrants est particulièrement faible lorsque les parents ont une scolarité nulle ou faible ou proviennent de milieux ruraux. En outre, nous montrons que le capital ethnique est également pertinent dans le pays d'origine des migrants.

  été trouvée non concluante parce que les individus pourraient craindre d'être capturés par les organisations criminelles pendant le voyage et migrer moins, alors que le crime fonctionne aussi comme une externalité négative poussant les individus à migrer. Notre variable sur les homicides ne contient que des données sur le taux de criminalité dans la municipalité de résidence au Mexique et ne peut donc pas prendre en compte l'effet sur le voyage du migrant. La comptabilisation de la distance et du taux de criminalité dans les états frontaliers a réussi à incorporer cet aspect et a eu un impact négatif sur la décision de migration illégale.

	Chapitre 1
	Avec tous ces faits stylisés à l'esprit, dans l'ensemble, cette thèse tente de fournir d'autres Le développement local et la décision de migrer : migration mexicaine vers les
	preuves sur la décision de migration et de mettre en évidence les effets nuisibles potentiels États-Unis
	de la migration sur le long terme. Ainsi, grâce à cette recherche, j'ai l'intention de fournir
	des implications politiques pour contribuer au bien-être des migrants mexicains. Cet article fournit un cadre théorique simple pour illustrer l'effet des investisments en
	développement local sur la décision de migrer illégalement. Cela montre que les politiques
	gouvernementales qui augmentent le développement local peuvent freiner les migrations, tout
	comme les coûts de migration et le crime organisé.
	En utilisant des données sur la migration en provenance du Mexique, nous testons da-
	vantage les prévisions du modèle et estimons la probabilité de décider de migrer vers les
	États-Unis en utilisant l'expression de désir

En s'ajoutant aux politiques d'immigration restrictives des États-Unis, une nouvelle menace pour les migrants a gagné en force ces dernières années. Avec la guerre des drogues du Mexique depuis 2006, les organisations criminelles ont trouvé un nouveau potentiel financier dans l'enlèvement et l'extorsion de migrants interceptés sur la longue trajectoire à travers le Mexique. Ainsi, en évitant d'être appréhendés par les autorités américaines à la frontière, les migrants craignent maintenant l'action des organisations criminelles en cours de route, les voies de migration typiques étant un point de risque pour l'enlèvement. Avec l'augmentation de la violence au Mexique, de nouvelles tendances dans la politique d'aide étrangère des États-Unis ont également émergé. En effet, si l'aide économique a été 1 réduite, elle a été remplacée par une aide militaire dans le but de lutter contre la criminalité. de migrer dans le future, disponible dans nos données pour contrôler les caractéristiques non observables des migrants. L'estimation par un modèle logit binomiale fournit des résultats favorables au modèle théorique proposé. Pourtant, il se pourrait aussi que l'effet soit différent entre les migrants légaux et les migrants illégaux. En effectuant le logit multinomial sur la spécification de base, les résultats suggèrent que le cadre théorique est valable pour les migrants illégaux alors qu'aucun résultat n'est trouvé pour soutenir le modèle pour le groupe des migrants légaux. Les résultats sont consolidés avec l'ajout de la richesse de la municipalité et des envois de fonds comme sources potentielles d'endogénéité. Nos résultats empiriques montrent que les résultats du développement ont un effet négatif sur la probabilité de migration illégale, mesurée par un indice de développement calculé par la méthode d'analyse des composants principaux, ou par une mesure de la qualité du système de soins de santé. Un proxy pour l'infrastructure de transport a été utilisé pour étudier l'effet des coûts de migration, les résultats empiriques se trouvent également en ligne avec le modèle, suggérant un effet positif et statistiquement significatif sur la probabilité de migration pour les deux types de migrants. Enfin, le crime organisé, appliqué par le taux d'homicides de la municipalité, donne un coefficient positif pour la migration illégale. Dans le cadre théorique, cette variable a Les résultats trouvés dans cet article éclairent l'effet des politiques du gouvernement mexicain sur les tendances migratoires au niveau local. En dépit de constater que les caractéristiques individuelles et familiales continuent de jouer un rôle important dans une telle décision, nous avons constaté des données probantes suggérant que l'augmentation des facteurs de développement à l'échelle locale peut empêcher les individus de subir une activité aussi dangereuse. En outre, nos résultats suggérent aussi que les programmes de transferts sociaux pourraient augmenter les taux de migration illégale à court terme, conformément à la littérature, car elle augmente les revenus actuels. Pourtant, l'effet à long terme pourrait être le contraire, compte tenu de l'effet négatif de l'éducation sur la migration illégale. Ni les variables de développement ni la criminalité organisée ne semblent avoir d'impact sur les migrants documentés. Seuls les coûts de migration semblent avoir un impact négatif, de même que certaines caractéristiques individuelles. Cela peut s'expliquer par une plus grande hétérogénéité dans le groupe légal, étant donné qu'il pourrait s'agir des migrants qui dépassent la validité légal de leur séjour autant que des migrants autorisés, aspect que nous ne pouvons pas discerner dans nos données.


Andreas Malcher

Hierarchies and Undecidability Results for Iterative Arrays with Sparse Communication

Iterative arrays with restricted internal inter-cell communication are investigated. A quantitative measure for the communication is defined by counting the number of uses of the links between cells and it is differentiated between the sum of all communications of an accepting computation and the maximum number of communications per cell occurring in accepting computations. The computational complexity of both classes of devices is investigated and put into relation. In addition, a strict hierarchy depending on the maximum number of communications per cell is established. Finally, it is shown that almost all commonly studied decidability questions are not semidecidable for iterative arrays with restricted communication and, moreover, it is not semidecidable as well whether a given iterative array belongs to a given class with restricted communication.

Introduction

Devices of homogeneous, interconnected, parallel acting automata have extensively been investigated from a computational capacity point of view. The specification of such a system includes the type and specification of the single automata (sometimes called cells), their interconnection scheme (which can imply a dimension to the system), a local and/or global transition function, and the input and output modes. Multidimensional devices with nearest neighbor connections whose cells are finite automata are commonly called cellular automata (CA). If the input mode is sequential to a distinguished communication cell, they are called iterative arrays (IA). In connection with formal language recognition IA have been introduced in [START_REF] Cole | Real-time computation by n-dimensional iterative arrays of finite-state machines[END_REF], where it was shown that the language family accepted by realtime-IA forms a Boolean algebra not closed under concatenation and reversal. In [START_REF] Chang | Parallel parsing on a one-way array of finite-state machines[END_REF] it is shown that for every context-free grammar a two-dimensional lineartime-IA parser exists. A realtime acceptor for prime numbers has been constructed in [START_REF] Fischer | Generation of primes by a one-dimensional real-time iterative array[END_REF]. A characterization of various types of IA in terms of restricted Turing machines and several results, especially speed-up theorems, are given in [START_REF] Ibarra | Some results concerning linear iterative (systolic) arrays[END_REF][START_REF] Ibarra | Two-dimensional iterative arrays: Characterizations and applications[END_REF]. Several more results concerning formal languages can be found, for example, in [START_REF] Smith | Real-time language recognition by one-dimensional cellular automata[END_REF][START_REF] Kutrib | Cellular automata and language theory[END_REF].

Communication is an essential resource for cellular automata and can be measured in a qualitative way and a quantitative way. In the first case, the number of different messages to be communicated by an IA is bounded by some fixed constant. Iterative arrays with this restricted inter-cell communication have been investigated in [START_REF] Umeo | A design of real-time non-regular sequence generation algorithms and their implementations on cellular automata with 1-bit inter-cell communications[END_REF][START_REF] Umeo | Real-time generation of primes by a 1-bit-communication cellular automaton[END_REF] with respect to the algorithmic design of sequence generation. In particular, it is shown that several infinite, non-regular sequences such as exponential or polynomial, Fibonacci, and prime sequences can be generated in real time. In connection with language recognition and decidability questions multi-dimensional iterative arrays and one-dimensional (one-way) cellular automata with restricted communication are intensively studied in [START_REF] Kutrib | Computations and decidability of iterative arrays with restricted communication[END_REF][START_REF] Kutrib | Cellular automata with limited inter-cell bandwidth[END_REF][START_REF] Worsch | Linear time language recognition on cellular automata with restricted communication[END_REF].

To measure the communication in cellular automata in a quantitative way we count the number of uses of the links between cells and we consider, on the one hand, bounds on the sum of all communications of an accepting computation and, on the other hand, bounds on the maximum number of communications per cell that may appear in accepting computations. Many results on this quantitative measure have been obtained for cellular automata in [START_REF] Kutrib | Cellular automata with sparse communication[END_REF][START_REF] Kutrib | One-way cellular automata, bounded languages, and minimal communication[END_REF], and cellular automata that are restricted with respect to the qualitative and the quantitative measure are investigated in [START_REF] Kutrib | On one-way one-bit O(1)-message cellular automata[END_REF][START_REF] Kutrib | One-way cellular automata, bounded languages, and minimal communication[END_REF] as well. As main results we would like to mention hierarchy results and the undecidability of almost all commonly studied decidability questions such as emptiness, finiteness, equivalence, inclusion, regularity, and context-freeness. It is of particular interest that even a small amount of communication is sufficient to obtain undecidability results.

In this paper, we want to continue the investigation of the quantitative measure by studying iterative arrays with quantitatively restricted communication. In the next section, we present some basic notions and definitions and we introduce the two classes of communication bounded iterative arrays, namely, sum communication bounded IA and max communication bounded IA. Moreover, we discuss several examples whose construction ideas are also helpful for other constructions in the sequel. In Section 3, we study the computational capacity of the introduced devices and obtain proper inclusions in between sum communication bounded IA and max communication bounded IA as well as between both classes. Sections 4 and 5 are devoted to studying decidability questions for sum communication bounded IA and max communication bounded IA. For the former class we obtain the non-semidecidability of emptiness, finiteness, equivalence, inclusion, regularity, and context-freeness for devices that have at most O(n) communications on accepted inputs of length n, whereas for the latter class all questions are not semidecidable as well for devices that have at most O(log(n)) communications per cell on accepted inputs of length n. Moreover, we can show for both classes that it is not semidecidable whether an arbitrary IA belongs to either class. It should be noted that missing proofs are omitted due to space limitations.

Definitions and Preliminaries

We denote the positive integers and zero {0, 1, 2, ...} by N. The empty word is denoted by λ, the reversal of a word w by w R , and for the length of w we write |w|. We use ⊆ for inclusions and ⊂ for strict inclusions. By log(n) we denote the logarithm of n to base 2. Throughout the article two devices are said to be equivalent if and only if they accept the same language.

A one-dimensional iterative array is a linear, semi-infinite array of identical deterministic finite state machines, sometimes called cells. Except for the leftmost cell each one is connected to its both nearest neighbors. For convenience we identify the cells by their coordinates, that is, by non-negative integers. The distinguished leftmost cell at the origin is connected to its right neighbor and, additionally, equipped with a one-way read-only input tape. At the outset of a computation the input is written on the input tape with an infinite number of end-of-input symbols to the right, and all cells are in the so-called quiescent state. The finite state machines work synchronously at discrete time steps. The state transition of all cells but the communication cell depends on the current state of the cell itself and on the information which is currently sent by its neighbors. The information sent by a cell depends on its current state and is determined by so-called communication functions. The state transition of the communication cell additionally depends on the input symbol to be read next. The head of the one-way input tape is moved to the right in each step. A formal definition is: Let M be an IA. A configuration of M at some time t ≥ 0 is a description of its global state which is a pair (w t , c t ), where w t ∈ A * is the remaining input sequence and c t : N → S is a mapping that maps the single cells to their current states. The configuration (w 0 , c 0 ) at time 0 is defined by the input word w 0 and the mapping c 0 that assigns the quiescent state to all cells, while subsequent configurations are chosen according to the global transition function ∆ that is induced by δ and δ 0 as follows: Let (w t , c t ), t ≥ 0, be a configuration. Then its successor configuration (w t+1 , c t+1 ) = ∆(w t , c t ) is as follows.

c t+1 (i) = δ(b r (c t (i -1)), c t (i), b l (c t (i + 1)))
for all i ≥ 1, and c t+1 (0) = δ 0 (a, c t (0), b l (c t (1))), where a = and w t+1 = λ if w t = λ, as well as a = a 1 and

w t+1 = a 2 • • • a n if w t = a 1 • • • a n .
An input w is accepted by an IA M if at some time i during the course of its computation the communication cell enters an accepting state. The language accepted by M is denoted by L(M ). Let t : N → N, t(n) ≥ n + 1 be a mapping. If all w ∈ L(M ) are accepted with at most t(|w|) time steps, then L(M ) is said to be of time complexity t.

The family of all languages which are accepted by some IA with time complexity t is denoted by L t (IA). If t is the function n + 1, acceptance is said to be in realtime and we write L rt (IA). Since for nontrivial computations an IA has to read at least one end-of-input symbol, realtime has to be defined as (n + 1)-time.

We remark that we obtain the classical definition of IA, if we set B = S and b l (s) = b r (s) = s for all s ∈ S.

In the following we study the impact of communication in iterative arrays. The communication is measured by the number of uses of the links between cells. It is understood that whenever a communication symbol not equal to ⊥ is sent, a communication takes place. Here we do not distinguish whether either or both neighboring cells use the link. More precisely, the number of communications between cell i and cell i + 1 up to time step t is defined by

com(i, t) = |{ j | 0 < j ≤ t and (b r (c j (i)) = ⊥ or b l (c j (i + 1)) = ⊥) }| .
For computations we now distinguish the maximal number of communications between two cells and the total number of communications. Let c 0 , c 1 , . . . , c t(|w|) be the sequence of configurations computed on input w by some iterative array with time complexity t(n), that is, the computation on w. Then we define

mcom(w) = max{ com(i, t(|w|)) | 0 ≤ i ≤ t(|w|) -1 } and scom(w) = t(|w|)-1 i=0 com(i, t(|w|)).
Let f : N → N be a mapping. If all w ∈ L(M ) are accepted with computations where mcom(w) ≤ f (|w|), then M is said to be max communication bounded by f . Similarly, if all w ∈ L(M ) are accepted with computations where scom(w) ≤ f (|w|), then M is said to be sum communication bounded by f . In general, it is not expected to have tight bounds on the exact number of communications but tight bounds on their numbers in the order of magnitude. For the sake of readability we denote the class of IA that are max communication bounded by some function g ∈ O(f ) by MC(f )-IA. In addition, we use the notation const for functions from O(1). The corresponding notation for sum communication bounded IA is SC(f )-IA.

To illustrate the definitions we start with some examples. Some of the ideas are also necessary for later constructions.

Example 2. The language { a n b 2n | n ≥ 1 } belongs to L rt (MC(const)-IA).
The idea of the construction is to start a signal with speed 1/2 to the right, that is, at every second time step the signal moves one cell to the right, when reading the first a. In addition, a signal with maximum speed to the right is started when the first b is read. When both signals meet, another signal with maximum speed is sent to the left and the input is accepted if and only if this signal reaches the communication cell when the last b is read. Since there are two right signals and one left signal used, it is clear that the IA constructed is an MC(const)-IA. An example computation on input a 5 b 10 is depicted in Figure 2 (left). The next example shows that a binary counter can already be implemented by an SC(n)-IA.

Example 4. The language { a n b n | n ≥ 1 } belongs to L rt (SC(n)-IA).
We implement the usual construction of a binary counter for IA (see, for example, [START_REF] Kutrib | Computations and decidability of iterative arrays with restricted communication[END_REF][START_REF] Kutrib | Cellular automata with limited inter-cell bandwidth[END_REF]), where the first log(n) cells store the binary encoding of some number n and the communication cell carries the least significant bit. To increase or decrease the counter we possibly have to send carry-overs in order to update the current encoding. Additionally, we mark the cell carrying the most significant bit suitably and this mark may move to the right while increasing the counter and may move to the left while decreasing the counter. Thus, to accept an input a n b n we start with a counter 0, we increase the counter by one for every read a and decrease the counter by one for every read b. If in the end the counter is 0 again, which can be detected with help of the mark of the most significant bit, and the input format is correct, we accept the input and reject in all other cases. An example computation may be found in Figure 3, where + resp. -denote carry-overs for increasing resp. decreasing the counter. Furthermore, the grey cells mark the cells carrying the most significant bit.

To calculate the number of necessary communications on an accepted input a n b n we observe that the only information sent to the right are the carry-overs, while the only information sent to the left is the position of the most significant bit. For the latter we have that there always is exactly one cell carrying the most significant bit which gives 2n communications. For the carry-overs it easy to see that the communication cell (cell 0) sends a carry-over in every second time step, while cell 1 sends a carry-over in every fourth time step, cell 2 sends a carry-over in every eighth time step and so on. Altogether, the number of communications for the carry-overs is bounded by

log(n) i=1 2n 2 i = 2n log(n) i=1 1 2 i = 2n 1 - 1 2 log(n) ≤ 2n 1 - 1 2 log(n)+1 = 2n 1 - 1 2n = 2n -1.
Hence, the number of communications on input a n b n is 2n + 2n -1 ∈ O(n) and the IA constructed is a realtime-SC(n)-IA. The symbols + resp. -denote carry-overs for increasing resp. decreasing the counter. The cells carrying the most significant bit are marked grey and g denotes an accepting state.

1 g + 0 1 0 0 0 + 0 1 0 1 0 0 0 1 - 1 1 1 0 0 0 + 0 0 - 1 1 0 0 1 - + 0 0 1 0 0 + 0 1 0 0 1 0 0 1 - 1 1 0 - 0 1 + 0 0 - 0 0 0 1 1 - 0 0 0 0 0 1 t ≥ 0 t ≥ 10 0 0 0 0 0 + 0 0
Example 5. The language { a 2 n b 2n | n ≥ 1 } belongs to L rt (SC(n)-IA). The rough idea is to implement a binary counter as in Example 4 which is increased for every input symbol a. When the first b is read, a right signal is started which inspects the counter and checks whether all cells are carrying a carry-over except the cell carrying the most significant bit. If so, the number of a's is 2 n for some n ≥ 1 and the signal is sent back to the left with maximum speed. When it reaches the communication cell exactly when the end-of-input symbol is read, then the input is accepted and in all other cases rejected.

Separability Results

In this section, we will separate several classes of max communication bounded and sum communication bounded iterative arrays. We start by showing that realtime-SC(n)-IA are less powerful than realtime-SC(n 2 )-IA. We remark that a similar result is known between realtime-SC(n)-CA and realtime-SC(n 2 )-CA (see, e.g., [START_REF] Kutrib | Cellular automata with sparse communication[END_REF]).

Theorem 6. L rt (SC(n)-IA) ⊂ L rt (SC(n 2 )-IA).
Proof. The inclusion follows from structural reasons. To show the properness of the inclusion we consider the language L = { wcw | w ∈ {a, b} + }, which can be accepted by using a queue store in which the first w part is enqueued. After the separating symbol c the queue store is symbolwise dequeued and matched with the second w part. It is shown in [START_REF] Kutrib | Cellular automata -a computational point of view[END_REF] how an IA can simulate such a queue store without any loss of time. Thus, L ∈ L rt (IA) which implies that L ∈ L rt (SC(n 2 )-IA). Another construction idea for L may be found in [START_REF] Cole | Real-time computation by n-dimensional iterative arrays of finite-state machines[END_REF]. On the other hand, let us assume that L belongs to L rt (SC(n)-IA). Then, we will derive a contradiction in two steps. First, it is possible under the above assumption to construct a realtime-SC(n

• √ n)-CA accepting L = { (wc) |w| | w ∈ {a, b} + }.
Second, by adapting the proof given in [START_REF] Kutrib | Cellular automata with sparse communication[END_REF] showing that { wcw R | w ∈ {a, b} + } does not belong to L rt (SC(f )-CA) if f ∈ o(n 2 / log(n)), we obtain that L does not belong to L rt (SC(n • √ n)-CA) as well which gives the desired contradiction. Now, let L be accepted by some realtime-SC(n)-IA M . A CA M accepting L works as follows on input wcwc • • • wc. M has six tracks. The original input is kept on track 1 without change. Each cell having as left neighbor a c-cell or the leftmost border cell can identify itself and will act on track 2 as communication cell for the simulation of M . The "input" is fed into the communication cells by shifting the input of the remaining cells on track 3 one cell to the left in every time step, whereby a second c acts as end-of-input symbol. The shifting is stopped before passing the second c-cell. Hence, every communication cell can decide after 2|w| + 2 time steps whether it has recognized the structure wcw and stores this information by entering some state g. On track 4, the rightmost cell starts a signal moving with maximum speed to the left that checks whether the input is correctly formatted and all communication cells have entered state g. Since the checked w-blocks are pairwise overlapping, we can check with this construction whether the input is of the form (wc) + for some w ∈ {a, b} + . It remains to check that the number of c's is exactly |w|. To this end, we use track 5 on which each c-cell sends a signal with maximum speed to the left. All incoming c-signals are collected on track 6 from left to right starting in the leftmost cell. This means that sending m c-signals leads to the marking of the leftmost m cells on track 6. Hence, the final signal on track 4 has additionally to check whether the leftmost w-block is completely marked on track 6. If this is the case, the input is accepted and in all other cases rejected. Hence, M accepts L in realtime. Next, we have to calculate the sum of all communications. The length of an accepted input is (

O(|w| 3 ). Therefore, M is a realtime-SC(n • √ n)-CA.
The proof that L does not belong to

L rt (SC(f )-CA) if f ∈ o(n 2 / log(n)
) is an adaption of a proof given in [START_REF] Kutrib | Cellular automata with sparse communication[END_REF] and omitted here.

For separating results in between the classes of max communication bounded iterative arrays we will use in the following the notion of time constructability. We say that a function f : N → N is time-constructible by an MC-IA M , if the communication cell of M enters, on empty input, a certain state exactly at the time steps f (n) for all n ≥ 1. For more information on time-constructible functions we refer to [START_REF] Kutrib | Cellular automata and language theory[END_REF][START_REF] Mazoyer | Signals in one-dimensional cellular automata[END_REF].

⊂ L rt (MC(const)-IA), 2. L rt (MC(const)-IA) ⊂ L rt (MC(log(n))-IA), 3. L rt (MC(log(n))-IA) ⊂ L rt (MC( √ n)-IA), 4. L rt (MC( √ n)-IA) ⊂ L rt (MC(n)-IA).
Proof. The inclusion claimed in 1. is clear, since the communication cell of an IA can simulate a deterministic finite automaton accepting a given regular language without using any communication. The inclusion is proper, since Example 2 provides a non-regular language accepted by a realtime-MC(const)-IA. The inclusions claimed in 2.-4. follow from structural reasons. Hence, it remains for us to show each properness. We start with the inclusion claimed in 2. and consider language L = { c 2 |w| wcw | w ∈ {a, b} + } for which we show that it belongs to L rt (MC(log(n))-IA), but not to L rt (MC(const)-IA). To construct a realtime-MC(log(n))-IA M for L we implement on track 1 the construction of 2 n given in Lemma 7. Additionally, we simulate on track 2 a queue store, where the top of the queue is located in the communication cell, and enter some symbol $ into the queue at every time step at which the communication cell recognizes a time step 2 n for n ≥ 1. Finally, we simulate on track 3 another queue store. As soon as the communication cell processes the first input symbol a or b from w, we check whether a time step 2 n has been identified in the last time step and we stop the computation on track 1. Additionally, we start to enter w to the queue on track 3 while for every symbol of w a symbol $ from the queue on track 2 is removed. When the separating symbol c is processed by the communication cell, we check whether the queue on track 2 is empty. If so, the number of initial c's has exactly been 2 |w| and we can continue to check the remaining input against the contents of the queue on track 3. Finally, the input is accepted if the check is positive and in all other cases the input is rejected. Next, we want to estimate the maximum number of communications per cell. An accepted input has a length of 2 |w| + 2|w| + 1. Due to Lemma 7 we know that at most O(|w|) communications take place on the first track. To enter |w| symbols into the queue on track 2 needs at most |w| communications per cell. Finally, at most 2|w| + 1 communications per cell can take place on track 2 and track 3 while processing the input suffix wcw. Altogether, at most O(|w|) communications take place per cell. Thus, L can be accepted by a realtime-MC(log(n))-IA.

To show that L is not accepted by any realtime-MC(const)-IA we combine two techniques which have successfully been applied for SC-CA [START_REF] Kutrib | Cellular automata with sparse communication[END_REF] and for IA with a bounded constant number of different messages to be communicated [START_REF] Kutrib | Cellular automata with limited inter-cell bandwidth[END_REF]. First, we derive an upper bound for the number of different communications that the communication cell can perform while processing an input of length n and performing communications. We have to take into account the information to be communicated and the time steps at which the communication takes place. Since there are n possibilities to choose time steps and |B| different messages to be sent, we obtain, for some constant k 0 ≥ 1, at most

n |B| ≤ n ( /2) /2 2 log(|B|) = n 2 /2 /2 2 log(|B|) = 2 log(n) + /2+log(|B|) -log( ) /2 ≤ 2 k0 log(n) = n k0
possibilities. Now, we assume that L is accepted by realtime-MC(const)-IA M and we denote by k the constant number of maximal communications per cell. Moreover, let c p be the configuration after processing the complete c-prefix of the input. Next, we want to calculate the number of different configurations of M starting in c p and processing the first w part of an input. Such a configuration depends on the information that has been sent to the IA via the communication cell and the current state of the communication cell. Hence, there are at most |w|

Undecidability Results for SC(n)-IA

In this section, we will show that almost all commonly studied decidability questions such as emptiness, finiteness, equivalence, inclusion, regularity, and context-freeness are not semidecidable for realtime-SC(n)-IA. Here, we say that a decision problem is decidable (undecidable) if the set of all instances for which the answer is "yes" is recursive (not recursive). A decision problem is said to be semidecidable if the set of all instances for which the answer is "yes" is recursively enumerable. It is known that the above-mentioned decidability questions are not semidecidable for realtime-IA [START_REF] Malcher | On the descriptional complexity of iterative arrays[END_REF]. Thus, the basic idea in the following is to find suitable languages that relate realtime-IA with realtime-SC(n)-IA. Let M be a realtime-IA over some alphabet A and a, b be symbols such that A ∩ {a, b} = ∅. Then, we define language

L M = wa 2 |w| b 2 |w| | w ∈ L(M ) . Lemma 9. Let M be a realtime-IA. Then, L M ∈ L rt (SC(n)-IA).
Proof. We sketch the construction of a realtime-SC(n)-IA M accepting L M . The IA M uses three tracks. Track 1 is used to simulate M where two cells of M are grouped into one cell of M . Track 2 is used to store in a queue for every input symbol from A a certain symbol $. When the first a-symbol is read, the first |w| cells of track 2 are marked with $. At this moment, we stop the simulation of M on track 1 and we start to increase a binary counter on track 3 as long as the input symbols are a. If the first b is read, we send a signal which checks whether the number of a's has been 2 |w| . This can be done by inspecting the counter and checking whether exactly all cells marked with $ have been used (see, e.g, Example 5). Additionally, we start to decrease the counter for every input symbol b. Finally, we accept the input if the counter has been decreased to zero and reject in all other cases.

The number of communications for the simulation of M on track 1 is bounded by O(|w| 2 ). The number of communications to mark the first |w| cells by $ and to stop the simulation is bounded by O(|w|). By observing that binary counters can be realized by SC(n)-IA, cf. Example 4, we know that the number of communications to increase the binary counter is bounded by O(2 |w| ). The number of communications to check that the number of a's has been 2 |w| is bounded by O(|w|). Finally, the number of communications to decrease the binary counter is bounded by O(2 |w| ) as well. Altogether, the number of all communications is bounded by in O(2 |w|+1 ). Since the input length is |w| + 2 |w|+1 , we obtain that the IA constructed is an SC(n)-IA. Now, the non-semidecidable property of realtime-IA M to accept the empty or a finite language, respectively, is reflected in properties of language L M which enable us in the next theorem to obtain the desired non-semidecidability results for realtime-SC(n)-IA.

Lemma 10. Let M be a realtime-IA. Proof. Claim 1 and claim 2 are obvious. It can be shown by a standard application of the pumping lemma that the language L M is not context-free, if L(M ) is infinite. On the other hand, if L(M ) is finite, L M is finite as well. This shows claim 3. and claim 4.

Theorem 11. Emptiness, finiteness, infiniteness, equivalence, inclusion, regularity, and context-freeness are not semidecidable for realtime-SC(n)-IA.

Proof. It is known that all above-mentioned questions are not semidecidable for realtime-IA due to the results given in [START_REF] Malcher | On the descriptional complexity of iterative arrays[END_REF]. By applying Lemma 9 and Lemma 10 we can immediately translate the non-semidecidability results to realtime-SC(n)-IA. Moreover, we cannot even semidecide the property of being sum communication bounded by n.

Theorem 12. It is not semidecidable for an arbitrary realtime-IA M whether or not M is a realtime-SC(n)-IA.

Finally, we can apply similar construction ideas as in Lemma 9 to separate the classes of realtime-MC(const)-IA and realtime-SC(n)-IA.

Theorem 13. L rt (MC(const)-IA) ⊂ L rt (SC(n)-IA).

Definition 1 .

 1 An iterative array (IA) is a system S, F, A, B, , s 0 , b l , b r , δ, δ 0 , where S is the finite, nonempty set of cell states, F ⊆ S is the set of accepting states, A ⊆ S is the finite, nonempty set of input symbols, B is the set of communication symbols, / ∈ A is the end-of-input symbol, s 0 ∈ S is the quiescent state, b l , b r : S → B ∪ {⊥} are communication functions which determine the information to be sent to the left and right neighbors, where ⊥ means nothing to send and b l (s 0 ) = b r (s 0 ) = ⊥, δ : (B ∪ {⊥}) × S × (B ∪ {⊥}) → S is the local transition function for non-communication cells satisfying δ(⊥, s 0 , ⊥) = s 0 , and δ 0 : (A ∪ { }) × S × (B ∪ {⊥}) → S is the local transition function for the communication cell.

a 1 aFigure 1 .

 11 Figure 1. An iterative array.

Figure 2 .Example 3 .

 23 Figure 2. Two example computations for Example 2 (left) on input a 5 b 10 and Example 3 (right) on input a 4 b 4 c 8 .

Figure 3 .

 3 Figure 3. Example computation for the construction given in Example 4 on input a 9 b 9 .The symbols + resp. -denote carry-overs for increasing resp. decreasing the counter. The cells carrying the most significant bit are marked grey and g denotes an accepting state.

Lemma 7 .

 7 The function 2 n can be time constructed by an MC(log(n))-IA. The function n 2 can be time constructed by an MC( √ n)-IA. Now, we can state the hierarchy of max communication bounded iterative arrays. Theorem 8. 1. REG

  |w| + 1)|w| = |w| 2 + |w| ∈ O(|w| 2 ). The number of communications on track 1 and track 6 is zero and in O(|w|), respectively. On track 2, we roughly have |w| simulations of M which has O(|w|) communications each by assumption. Hence, track 2 has at most O(|w| 2 ) communications. On track 3, we shift blocks of length 2|w| + 2 for O(|w|) many time steps which causes at most O(|w| 2 ) communications in the whole. On track 4 we have O(|w| 2 ) communications, since the signal passes the complete input. Finally, on track 5 we have |w| signals passing at most O(|w| 2 ) cells which gives at most O(|w| 3 ) communications. Altogether, the sum of all communications in M is in

  k0•k • |S| different configurations, where S denotes the state set of M . On the other hand, there are 2 |w| different words w. Now, we choose |w| large enough such that 2 |w| is larger than the polynomial |w| k0•k • |S|. Then, there are two different words w = w such that |w| = |w | and M enters the same configuration after processing c 2 |w| w as well as after processing c 2 |w| w . Since the input c 2 |w| wcw is accepted, input c 2 |w| w cw is accepted as well which is a contradiction. The proof of claim 3. is similar. We consider L = { c |w| 2 wcw | w ∈ {a, b} + } and can construct in a similar way as above an MC( √ n)-IA accepting L in realtime by taking into account that Lemma 7 shows that at most O(|w|) communications per cell are necessary to time construct |w| 2 . To show with the above technique that L is not accepted by any realtime-MC(log(n))-IA it is sufficient to choose |w| large enough such that 2 |w| > |w| k0 log(|w|) • |S|. This is possible since the latter inequality is equivalent to |w| > k 0 • |S| • log(|w|) • log(|w|) which holds for |w| large enough. Finally, we show 4. by considering L = { wcw | w ∈ {a, b} + } which is obviously accepted by a realtime-MC(n)-IA. On the other hand, we have to choose |w| large enough such that 2 |w| > |w| k0 √ |w| • |S| which is equivalent to |w| > k 0 • |S| • log(|w|) • |w| and holds for |w| large enough.

  1. L M is empty if and only if L(M ) is empty. 2. L M is finite if and only if L(M ) is finite. 3. L M is regular if and only if L(M ) is finite. 4. L M is context-free if and only if L(M ) is finite.

Acknowledgment

Thanks are given to Victor Roussanaly for several discussions on the topic while his internship at our institute in 2014.

Undecidability Results for MC(log(n))-IA

In this section, we prove similar non-semidecidability results for MC(log(n))-IA by using similar methods as in the previous section. Let M be a realtime-IA over some alphabet A and c be a symbol such that A ∩ {c} = ∅. Then, we define language

The proof of the following lemma and the following theorem is nearly identical to the proof of Lemma 10 and of Theorem 11, respectively. Lemma 15. Let M be a realtime-IA.

Theorem 16. Emptiness, finiteness, infiniteness, equivalence, inclusion, regularity, and context-freeness are not semidecidable for realtime-MC(log(n))-IA.

Finally, we cannot even semidecide the property of being max communication bounded by log(n).

Theorem 17. It is not semidecidable for an arbitrary realtime-IA M whether or not M is a realtime-MC(log(n))-IA.

We remark that it is currently an open question whether or not all discussed decidability questions are not semidecidable for realtime-MC(const)-IA as well.