P Durand Estebe

V Boitier

M Bafleur

J-M Dilhac
email: dilhac@laas.fr

Power Supply for a Wireless Sensor Network: Airliner Flight Test Case Study

Keywords: Flight Tests, Sensor Network, Solar Energy, Ultracapacitors. I

In this paper we present hands-on experience related to on-going implementation in aircraft of power supply for a wireless sensor network deployed for aerodynamic flight tests. This autonomous battery-free power supply is capturing, managing and storing primary energy from the environment, using solar light and photovoltaic cells. For practical purposes, it is also equipped with an auxiliary power input. The specifications are detailed, the general architecture is presented and justified, and test results are discussed.

INTRODUCTION

Air transport is now an essential pillar of modern society, and a major driver of global economic prosperity. Aviation forecasts show massive traffic increase, both for passengers and cargo, in the next decades. Therefore, air transport is facing various challenges such as fossil fuel consumption, pollutant and noise emission, air traffic congestion, business model, safety and security.

Technological innovations are therefore pursued in the area -among others -of engines, aircraft structural design, and structural new materials. Other innovations are taking place through the concept of More Electric Aircraft (MEA) that is an evolution starting with fly-bywire (a full electronic interface replaces the classical electro-mechanical interface between pilots and aircraft systems), and evolving through drive-by-wire (no more physical connection -mechanical, pneumatic or hydraulic -between sensor and actuator) to power-bywire (where pneumatic, mechanical and hydraulic power distributions are replaced by an electric power grid, except for propulsive power) [START_REF] Rosero | Moving Towards a More Electric Aircraft[END_REF]. It is worth to mention that MEA obviously calls for an increase in electrical power wiring size and complexity.

However, aviation's progress will also be carried out by an increased integration of cyber-physical systems into aircraft [START_REF] Sampigethaya | Aviation Cyber-Physical Systems: Foundations for Future Aircraft and Air Transport[END_REF] for managing baggage, cargo, personal electronic devices, flight deck tasks and helping maintenance through Structural Health Monitoring (SHM) [START_REF] Santos | Embraer Perspective on the Introduction of SHM into Current and Future Commercial Aviation Programs[END_REF]. There again the weight of wiring is likely to increase.

In that context, Wireless Sensor Networks (WSN) have been considered for various aeronautical applications, such as SHM [START_REF] Dilhac | Energy Thermo Generation in Aeronautics for Battery-free Wireless Sensor Networks[END_REF] and flight tests. Each node of this network would perform sensing, data processing and wireless transmission of information. Such wireless networks will hopefully permit (often new) functions without the need of adding extra wiring to an already large burden.

However, these nodes need to be self-powered, many of the advantages of wireless sensor networking being obviously lost if external (i.e. wired) power sources were used. For this purpose, batteries offer a high energy density at low cost. However, there are critical drawbacks associated with the use of batteries: first environmental concerns and economical aspects associated with the replacement of primary batteries. Second, batteries (either primary or secondary) may be prohibited since the wireless nodes are often implemented in locations without temperature regulation that could result both in a drastically reduced yield together with safety issues. Fortunately, batteries can be avoided through the use of environmental energy capture allowing a solution for long term, deploy and forget, WSN. However, environmental energy transducers, unlike batteries, are not energy reservoirs, and energy buffer storage is mandatory whatever the context. We will explain why it can be achieved through electrostatic ultracapacitors (UC).

In this paper we present hands-on experience related to on-going implementation of energy harvesters in airliners for the purpose of flight tests. Even if aircraft manufacturers alone are involved in this application, this issue is critical as the implementation in the experimental aircraft of the extra wiring required for flight tests is complex and time-consuming.

In the second section we will describe the requirements of our application, and we will present the devised architecture in the third section. In a fourth section we will present preliminary results and identify directions for future work in the conclusion.

II. SYSTEM GLOBAL REQUIREMENTS

In Fig. 1 the total electric cable lengths implemented in a car, a jet fighter and an airliner are compared. These lengths are also converted in kilometer per unit length of the car/aircraft as a measurement of complexity. From Fig. 1, it appears that fighter jets and airliners are very complex objects considering wiring, thus praising for wireless solutions when the deployment of new avionic is considered. As a consequence of such a choice, measurement data need of course to be transmitted wirelessly and the device has to be autonomous in energy. Specific components are therefore required to allow for this autonomy. Nevertheless, if stringent weight constraints (common in aeronautics) cannot afford these extra components, and if a power line runs close by, a connection to this line will be preferred. Fig. 1 also gives the extra wiring related to flight tests, i.e. 60% of the regular wiring in the case of the A380. Generally speaking, this wiring is often difficult to implement and may be realized by bonding the cables using adhesive tapes for the instrumentation outside aircraft structure, or passing cables through multiple bulkheads by removing screws, bolts or rivets, or even by drilling holes when permitted (rarely allowed in composite materials) that is a cumbersome process, not to mention the multiplication of connectors. So, even if the application detailed in this paper is of interest to flight test departments of aircraft manufacturers only, it is a critical issue because flight-testing is essential to validate a design and obtain certifications from government agencies, while being expensive, complex and timeconsuming.

total cable length (km) total cable length per unit length (km/m)

1 10 100
Eurofighter Typhoon (15.9 m) Among the typical measurements performed during flight-tests, are pressure sensing at tens of positions around wings, tail, rudder… For this purpose, pressure gloves, themselves accommodating tens of sensors are affixed to the aircraft outside skin together with cables connecting them to data loggers. The replacement of this apparatus by WSN (Fig. 2) would reduce design load, installation and relocation time.

Considering that a wireless implementation is chosen, the simplest way of gaining autonomy in energy is to use an energy reservoir such as a primary electrochemical battery. Such batteries are products of a mature industry: they offer a high energy density -and even a high power density when in parallel with an ultracapacitor -together with a low self-discharge. But, as already mentioned, their performance is strongly altered by the extreme (low) temperature encountered outside aircraft at cruise altitude, not to mention safety issues raised by some technologies. Energy capture from the environment is then mandatory and fortunately, for the considered application, solar energy can be harvested because i) the sensors are located outside the aircraft ii) for security and simplicity reasons most flight tests are done at daylight.

It is worth mentioning that energy storage is here still required for two reasons: first to accommodate for transient power surges from the load exceeding the mean electrical harvested power, and then to maintain the energetic autonomy in the case of an intermittent environmental source as will be illustrated later. UC performing electrostatic storage may do the job; while being affected by extreme positive ambient temperatures similarly to most batteries, they exhibit better performance at low temperature and provide an almost infinite lifetime. Consequently, they do not need any replacement. Because of their low energy density, they are safer than batteries, and supposed to be more environment-friendly. Unfortunately, they are impaired by strong self-discharge especially during the first hours [START_REF] Diab | Self-Discharge Characterization and Modeling of Electrochemical Capacitor Used for Power Electronics Applications[END_REF] and efficient long-term storage is not feasible. Finally, they exhibit a charge-dependent output voltage asking for a voltage regulator when used for circuit biasing, and suffer from a low maximum voltage rating (as low as 2.2V for some models tested below) related to the dielectric properties of the electrolyte.

Solar energy is qualitatively one of the most abundant ambient energy and easily translates itself into electricity through mature and still progressing technology, while UC are an appealing alternative to batteries but, for supplying power to the above pressure sensors, specific requirements from the environment are to be fulfilled. They are two fold.

First, the power supply (comprising photovoltaic cells, maximum power point tracking circuit, energy management devices and buffer storage ultra capacitor) must be both very thin not to disturb the streamline flow, and globally flexible to adapt to curvy profiles. Considering areas, flexibility main impact is on photovoltaic (PV) cells, restricting the choice to less efficient cell technologies.

Then, all devices must operate at low temperature (down to -55°C) and reduced atmospheric pressure (200hPa); fortunately low temperatures have a favorable impact on PV cell yield. Conversely, references of energy buffer UC correctly performing at such extreme temperatures and ambient pressure must be identified.

Finally the amount of power delivered to the sensing and communicating devices has to be assessed, given the sampling frequency, number of sensors and wireless data rate.

This system development has to be carefully carried out, considering the environment (i.e. solar flux vs. altitude, time, season, location…) and the harvesting system itself (photovoltaic cells and associated electronics). However, the objective is not to install a permanent system aiming at monitoring a critical parameter during the airliner lifetime, but to deploy a temporary test rig using WSN. Long-term dependability is then not at stake.

In the next section we will now detail quantitative requirements and derive the general architecture for the power supply unit.

III. GENERAL ARCHITECTURE

General requirements of our application translate into the following. The flexible power supply dedicated to be bonded to the extrados of an aircraft wing (see Fig. 2): -uses solar cells as main source of energy, -is less than a few millimeters in thickness, -delivers a mean electrical power of at least 2W under 5V (later shifted to 48V, see below), under modest (cloudy) illumination, -operates between -50°C (cruise altitude) and +85°C (parking under direct sunlight), and down to 200hPa (i.e. 35 000feet),

-incorporates an energy storage (UC) unit in order to deal with transient absence of sunlight, the targeted autonomy being 1 hour, -is capable of autonomous start-up, with the help of solar cells alone, the storage unit being empty [START_REF] Boitier | Under voltage lock-out design rules for proper start-up of energy autonomous systems powered by supercapacitors[END_REF].

The typical use case is illustrated in Fig. 3. Considering the above specifications, we devised the general architecture depicted in Fig. 4. The load corresponds to a datalogger used to manage the pressure measurement sensors; its typical characteristics are in the range 48V / 2W. The PV cells are connected to a power conditioner whose task is to optimize the energy transfer through Maximum Power Point Tracking (MPPT) and to store the energy in the UC. It also protects the UC from overvoltage. A blocking diode is inserted between power conditioning and UC to prevent the latter from discharging itself when photovoltaic cells are not delivering any energy.

The UC is connected to the load through a boost regulator. In a start-up phase, as long as regulator input voltage is below min operating value, power conditioner does not bias the regulator, in order to speed-up UC charge.

IV. EXPERIMENTAL RESULTS

For the solar cell testing, key points were a flexible photovoltaic panel with the best efficiency at low light, as the system has to power the load even in cloudy weather. We used thin film solar cells, reaching 9% efficiency at 72 W/m². Fig. 5 shows flexibility and main characteristics of the selected PV panel (SolbianFlex SP50-L). Considering energy storage, we tested 8 types of UC from six different manufacturers in climatic chambers to identify technologies compatible with our requirements. According to data sheets, the operating temperatures were ranging between [-20, +70°C] and [-40, +85°C] depending upon model. In other words, no model was initially rated for the extended range of [-50, +85°C].

With a SP-240 4A potentiostat from BioLogic, we first submitted the devices to constant current charges and discharges in a Temptronic Thermostream climatic chamber, at temperatures between -50°C and +100°C. Then, at -50°C only, we submitted them to an identical charge and discharge cycle, at 200hPa, in another climatic chamber (CLIMATS EX5423-TE).

During these two sets of experiments, we plotted the V(t) curves and the drift vs. temperature (see the example of Fig. 6). Finally, we measured the self-discharge performance in open circuit of all models by plotting, during more than three days, the output voltage vs. time after an initial charge at 2.2V.

From the above tests we made a trade-off and identified the best reference, also considering both thickness and capacitance per cm 2 , in order to comply with the already mentioned thickness requirements and to minimize the area devoted to energy storage. Nevertheless, the targeted autonomy asked for the association of multiple UCs.

We then devised an electronic circuit (see Fig. 7) incorporating all devices shown in Fig. 4 except PV cells and the ground power supply. We carefully limited the thickness of the circuit, specifically that of the inductor. Many electronic devices, such as the microcontroller and the converters, require a bias voltage. For this purpose, a 5 volts LDO voltage regulator TPS71550 (Vout = 5V , 6V ≤Vin ≤ 24V) is directly connected to solar panel. Consequently, if the photovoltaic voltage falls under 6V, the Power Conditioning device in between photovoltaic panel and UCs is cut off and, the load is powered by UCs only. This Power Conditioning is a DC/DC synchronous buck converter in series with a blocking Schottky diode.

To deal with various atmospheric conditions, a MPPT algorithm is implemented in a PIC18F1220 microcontroller based upon fractional Open-Circuit Voltage Method with the advantage of using one sensor only. The open circuit voltage of photovoltaic cells is measured every 10 seconds. When the UCs voltage reaches almost its maximum rated value, the algorithm will move from MPPT mode to UC voltage regulation mode.

The output stage was first designed to deliver a 5V output. Because of late changes in specifications requiring a 48V output, we simply add a 5V to 48V boost regulator due to a lack of time for another solution.

A boost regulator (LT3539) is placed between the UCs and the load in order to regulate the output voltage to 5V. The input voltage range of this component is 2.3-4.4V when it supplies 2W.

We used LT3539 Shutdown pin to keep the output disabled and to allow the photovoltaic panel to first charge UCs [START_REF] Boitier | Under voltage lock-out design rules for proper start-up of energy autonomous systems powered by supercapacitors[END_REF]. When the UCs terminal voltage reaches 4V (the higher the voltage across the UCs, the better the LT3539 efficiency is), the LT3539 is turned on by a command from the microcontroller. Then the solar panel will both power the load and charge the UCs whenever the sun is shining strongly enough. If not, the UCs alone will power the load.

The 5V to 48V conversion is realised by a MAX1523 boost controller, supplied by the LT3539 output, and thus is only activated when the LT3539 is on.

Finally, for the bonding onto the aircraft wing, the electronic power management board together with ultracapacitors was inserted into a thin plastic packaging whose shape was designed in order to minimize disorders induced to the airflow. Pictures of this arrangement are shown in Fig. 8. Paths for cables to the photovoltaic panel and the sensors are set up in the beveled edges of the packaging.

The overall system supplies the 2W load from a solar irradiance as low as 80W/m² using a 0.32m² SolbianFlex SP50L PV panel, rated with peak power of 50W.

V. CONCLUSIONS

We have reported the design details of a power supply for a wireless sensor network deployed for airliners inflight tests. The system has been successfully tested on ground. Real flight-tests are scheduled to confront with real environment.

Fig. 1 .

 1 Fig. 1. Wiring complexity for various means of transportation (estimations).

Fig. 2 .

 2 Fig. 2. Schematic of pressure gloves affixed on top of a wing. The system here is supposed wireless.

Fig. 3 .

 3 Fig. 3. Power supply: example of a use case as given by the final user. FL stands for Flight Level, and roughly corresponds to an altitude in hundreds of feet.

Fig. 4 .

 4 Fig. 4. Power supply: general architecture. Power conditioning includes MPPT (Maximum Power Point Tracking), UC overvoltage protection and buck-boost regulator command (not shown).

Fig. 5 .

 5 Fig. 5. Main characteristics of SolbianFlex SP50-L.

Fig. 6 .

 6 Fig. 6. Variations of capacitance and ESR with temperature and example of charge and discharge of a Maxwell PC10 ultracapacitor. The voltage drop after the peak is due to the equivalent serie resistor of the UC.

Fig. 7 .

 7 Fig. 7. Power management board.

Fig. 8 .

 8 Fig. 8. (a) power management module and ultracapacitors inserted into package (b) package as it will appear once bonded to the aircraft wing.


Zoltán Ésik

Uli Fahrenberg

Axel Legay

* -Continuous Kleene ω-Algebras *

We define and study basic properties of * -continuous Kleene ω-algebras that involve a * -continuous Kleene algebra with a * -continuous action on a semimodule and an infinite product operation that is also * -continuous. We show that * -continuous Kleene ω-algebras give rise to iteration semiring-semimodule pairs. We show how our work can be applied to solve certain energy problems for hybrid systems.

Introduction

A Kleene algebra [START_REF] Kozen | A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events[END_REF] is an idempotent semiring S = (S, ∨, •, ⊥, 1) equipped with a star operation * : S → S such that for all x, y ∈ S, yx * is the least solution of the fixed point equation z = zx ∨ y and x * y is the least solution of the fixed point equation z = xz ∨ y.

Examples of Kleene algebras include the language semiring P (A * ) = (P (A * ), ∨, •, ⊥, 1) over an alphabet A, whose elements are the subsets of the set A * of all finite words over A, and whose operations are set union and concatenation, with the languages ∅ and {ǫ} serving as ⊥ and 1. Here, ǫ denotes the empty word. The star operation is the usual Kleene star: X * = n≥0 X n = {u 1 . . . u n : u 1 , . . . , u n ∈ L, n ≥ 0}, for all X ⊆ A * .

Another example is the Kleene algebra P (A × A) = (P (A × A), ∨, •, 0, 1) of binary relations over any set A, whose operations are union, relational composition (written in diagrammatic order), and where the empty relation ∅ and the identity relation id serve as the constants ⊥ and 1. The star operation is the formation of the reflexive-transitive closure, so that R * = n≥0 R n for all R ∈ P (A × A).

The above examples are in fact continuous Kleene algebras, i.e., idempotent semirings S such that equipped with the natural order, they are all complete lattices (hence all suprema exist), and the product operation preserves arbitrary suprema in either argument: y( X) = yX and ( X)y = Xy for all X ⊆ S and y ∈ S. The star operation is given by x * = n≥0 x n , so that x * is the supremum of the set {x n : n ≥ 0} of all powers of x. It is well-known that the language semirings P (A * ) may be identified as the free continuous Kleene algebras (in a suitable category of continuous Kleene algebras).

A larger class of models is given by the * -continuous Kleene algebras [START_REF] Kozen | A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events[END_REF]. By the definition of * -continuous Kleene algebra S = (S, ∨, •, ⊥, 1), only suprema of sets of the form {x n : n ≥ 0} need to exist, where x is any element of S, and x * is given by this supremum. Moreover, product preserves such suprema in both of its arguments:

y( n≥0 x n ) = n≥0
yx n and ( n≥0

x n )y = n≥0

x n y.

For any alphabet A, the collection R(A * ) of all regular languages over A is an example of a * -continuous Kleene algebra which is not a continuous Kleene algebra. The Kleene algebra R(A * ) may be identified as the free * -continuous Kleene algebra on A. It is also the free Kleene algebra on A, cf. [START_REF] Kozen | On Kleene Algebras and Closed Semirings[END_REF]. There are several other characterizations of R(A * ), the most general of which identifies R(A * ) as the free iteration semiring on A satisfying the identity 1 * = 1, cf. [START_REF] Bloom | Iteration Theories -The Equational Logic of Iterative Processes[END_REF][START_REF] Krob | Complete Systems of B-Rational Identities[END_REF].

For non-idempotent extensions of the notions of continuous Kleene algebras, * -continuous Kleene algebras and Kleene algebras, we refer to [START_REF] Ésik | Rationally additive semirings[END_REF][START_REF] Ésik | Inductive * -semirings[END_REF].

When A is an alphabet, let A ω denote the set of all ω-words (sequences) over A. An ωlanguage over A is a subset of A ω . It is natural to consider the set P (A ω ) of all languages of ω-words over A, equipped with the operation of set union as ∨ and the empty language ∅ as ⊥, and the left action of P (A * ) on P (A ω ) defined by XV = {xv : x ∈ X, v ∈ V } for all X ⊆ A * and V ⊆ A ω . It is clear that (P (A ω ), ∨, ⊥) is in fact a P (A * )-semimodule and thus (P (A * ), P (A ω )) is a semiring-semimodule pair. We may also equip (P (A * ), P (A ω )) with an infinite product operation mapping an ω-sequence (X 0 , X 1 , . . .) over P (A * ) to the ω-language n≥0 X n = {x 0 x 1 . . . ∈ A ω : x n ∈ X n }. (Thus, an infinite number of the x n must be different from ǫ. Note that 1 ω = ⊥ holds.) The semiring-semimodule pair so obtained is a continuous Kleene ω-algebra.

More generally, we call a semiring-semimodule pair (S, V ) a continuous Kleene ω-algebra if S is a continuous Kleene algebra (hence S and V are idempotent), V is a complete lattice with the natural order, and the action preserves all suprema in either argument. Moreover, there is an infinite product operation which is compatible with the action and associative in the sense that the following hold for all x, x 0 , x 1 , . . . ∈ S:

• x( n≥0 x n ) = n≥0 y n , where y 0 = x and y n = x n-1 for all n > 0,

• n≥0 x n = k≥0 y k , whenever there is a sequence of integers 0 = i 0 ≤ i 1 ≤ . . . increasing without a bound such that

y k = x i k • • • x i k+1 -1 for all k ≥ 0.
Moreover, the infinite product operation preserves all suprema:

• n≥0 ( X n ) = { n≥0 x n : x n ∈ X n , n ≥ 0},
for all X 0 , X 1 , . . . ⊆ S.

The above notion of continuous Kleene ω-algebra may be seen as a special case of the not necessarily idempotent complete semiring-semimodule pairs of [START_REF] Ésik | On iteration semiring-semimodule pairs[END_REF].

Our aim in this paper is to provide an extension of the notion of continuous Kleene ω-algebras to * -continuous Kleene ω-algebras which are semiring-semimodule pairs (S, V ) consisting of a * -continuous Kleene algebra S = (S, ∨, •, ⊥, 1) acting on a necessarily idempotent semimodule V = (V, ∨, ⊥), such that the action preserves certain suprema in its first argument, and which are equipped with an infinite product operation satisfying the above compatibility and associativity conditions and some weaker forms of the last axiom. We will define both a finitary and a non-finitary version of * -continuous Kleene ω-algebras.

We will establish several properties of * -continuous Kleene ω-algebras, including the existence of the supremum of certain subsets related to regular ω-languages. Then we will use these results in our characterization of the free * -continuous Kleene ω-algebras, at least in the finitary version.

When (S, V ) is a * -continuous Kleene algebra, we may define an omega operation S → V by x ω = n≥0 x n , where x n = x for each n ≥ 0. One of or results will show that equipped with this omega operation, each * -continuous Kleene ω-algebra gives rise to an iteration semiringsemimodule pair. This extends the known result that each * -continuous Kleene algebra is an iteration semiring.

Part of this work is motivated by an application to so-called energy problems for hybrid systems.

When modeling systems with constraints on energy consumption, it is of interest to know whether certain states are reachable under the given energy constraints, or whether the system admits an infinite run. In the context of formal modeling and verification, such problems were first taken up in [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF], which spurned a number of other papers on similar problems.

We have shown in [START_REF] Ésik | Kleene algebras and semimodules for Energy Problems[END_REF] that most of these problems can be covered by a new abstract notion of energy automaton, which is a finite automaton in which the transitions are labeled with functions which map input energy to output energy. The intuition is that the transitions of an energy automaton are energy transformations, so given an initial energy, one can ask whether a final state is reachable when starting with this initial energy, or whether there is a Büchi run given this initial energy.

We will show in the later parts of this paper that energy functions form a finitary *-continuous Kleene ω-algebra, hence that energy problems can be solved using the techniques developed here.

Semirings and semiring-semimodule pairs

Although we already mentioned semirings and semimodules in the introduction, in this section we briefly recall the main definitions from [START_REF] Berstel | Noncommutative Rational Series With Applications[END_REF][START_REF] Golan | Semirings and their Applications[END_REF] in order to make the paper self-contained.

Recall from [START_REF] Berstel | Noncommutative Rational Series With Applications[END_REF][START_REF] Golan | Semirings and their Applications[END_REF] that a semiring S = (S, +, •, 0, 1) consists of a commutative monoid (S, +, 0) and a monoid (S, •, 1) such that the distributive laws

x(y + z) = xy + xz (y + z)x = yx + zx
and the zero laws 0 • x = 0 = x • 0 hold for all x, y, z ∈ S. It follows that the product operation distributes over all finite sums.

An idempotent semiring is a semiring S whose sum operation is idempotent, so that x + x = x for all x ∈ S. Each idempotent semiring S is partially ordered by the relation x ≤ y iff x + y = y, and then sum and product preserve the partial order and 0 is the least element. Moreover, for all x, y ∈ S, x + y is the least upper bound of the set {x, y}. Accordingly, in an idempotent semiring S, we will usually denote the sum operation by ∨ and 0 by ⊥.

In addition to semirings, we will also consider semiring-semimodule pairs. Suppose that S = (S, +, •, 0, 1) is a semiring and V = (V, +, 0) a commutative monoid. When V is equipped with a left S-action S × V → V , (s, v) → sv, satisfying

(s + s ′ )v = sv + s ′ v s(v + v ′ ) = sv + sv ′ (ss ′ )v = s(s ′ v) 0s = 0 s0 = 0 1v = v
for all s, s ′ ∈ S and v ∈ V , then we call V a (unitary left) S-semimodule and (S, V ) a semiringsemimodule pair. Note that when S is idempotent, then V is necessarily idempotent, so that we use the notation (V, ∨, ⊥).

Free continuous Kleene ω-algebras

We have defined continuous Kleene ω-algebras in the introduction as idempotent semiringsemimodule pairs (S, V ) such that S = (S, ∨, •, ⊥, 1) is a continuous Kleene algebra and V = (V, ∨, ⊥) is a continuous S-semimodule. Thus, equipped with the natural order, ≤, S and V are complete lattices and the product and the action preserve all suprema in either argument. Moreover, there is an infinite product operation, satisfying the compatibility and associativity conditions, which preserves all suprema.

In this section, we offer descriptions of the free continuous Kleene ω-algebras and the free continuous Kleene ω-algebras satisfying the identity 1 ω = ⊥.

A homomorphism between continuous Kleene algebras preserves all operations. A homomorphism is continuous if it preserves all suprema. We recall the following basic result.

Theorem 3.1 For each set A, the language semiring (P (A * ), ∨, •, ⊥, 1) where ∨ is set union,

• is concatenation and the constants ⊥ and 1 are ∅ and {ǫ}, respectively, is the free continuous Kleene algebra on A.

Thus, if S is a continuous Kleene algebra and h : A → S is any function, then there is a unique continuous homomorphism h ♯ : A * → S extending h.

In view of Theorem 3.1, it is not surprising that the continuous Kleene ω-algebras can be described using languages of finite and ω-words.

Suppose that A is a set. Let A ω denote the set of all ω-words over A, and let A ∞ = A * ∪ A ω . Let P (A * ) denote the language semiring over A, and let P (A ∞ ) denote the semimodule of all subsets of A ∞ equipped with the action of P (A * ) defined by XY = {xy : x ∈ X, y ∈ Y } for all X ⊆ A * and Y ⊆ A ∞ . We also define an infinite product by n≥0 X n = {u 0 u 1 . . . : u n ∈ X n }. Note that P (A ω ) is a subsemimodule of P (A ∞ ).

Proposition 3.2 For each set A, (P (A * ), P (A ∞ )) is a continuous Kleene ω-algebra.

Homomorphisms between continuous Kleene ω-algebras (S, V ) and (S ′ , V ′ ) consist of two functions h S : S → S ′ and h V : V → V ′ that together preserve all operations. A homomorphism (h S , h V ) is continuous if h S and h V preserve all suprema.

Theorem 3.3 (P (A * ), P (A ∞ )) is the free continuous Kleene ω-algebra, freely generated by A.

Proof. Suppose that (S, V ) is any continuous Kleene ω-algebra an let h : A → S be a mapping. We want to show that there is a unique extension of h to a continuous homomorphism (h ♯ S , h ♯ V ) from (P ω (A), P (A ∞ )) to (S, V ).

For each u = a 0 . . . a n-1 in A * , define h S (u) = h(a 0 ) • • • h(a n-1 ) and h V (u) = h(a 0 ) • • • h(a n-1 )1 ω = k≥0 b k , where b k = a k for all k < n and b k = 1 for all k ≥ n. When u = a 0 a 1 . . . ∈ A ω , define h V (u) = k≥0 h(a k ). Note that we have h S (uv) = h S (u)h S (v) for all u, v ∈ A * and h S (ǫ) = 1. Also, h V (uv) = h S (u)h V (v) for all u ∈ A * and v ∈ A ∞ . Thus, h V (XY ) = h S (X)h V (Y ) for all X ⊆ A * and Y ⊆ A ∞ . Moreover, for all u 0 , u 1 , . . . in A * , if u i = ǫ for infinitely many i, then h V (u 0 u 1 . . .) = k≥0 h S (u k ). If on the other hand, u k = ǫ for all k ≥ n, then h V (u 0 u 1 . . .) = h S (u 0 ) • • • h S (u n-1 )1 ω . In either case, if X 0 , X 1 , . . . ⊆ A * , then h V ( n≥0 X n ) = n≥0 h S (X n ). Suppose now that X ⊆ A * and Y ⊆ A ∞ . We define h ♯ S (X) = h S (X) and h ♯ V (Y ) = h V (Y ). It is well-known that h ♯ S is a continuous semiring morphism P (A * ) → S. Also, h ♯ V preserves arbitrary suprema, since h ♯ V ( i∈I Y i ) = h V ( i∈I Y i ) = i∈I h V (Y i ) = i∈I h V (Y i ) = i∈I h ♯ V (Y i ).
We prove that the action is preserved.

Let X ⊆ A * and Y ⊆ A ∞ . Then h ♯ V (XY ) = h V (XY ) = h S (X)h V (Y ) = h S (X) h V (Y ) = h ♯ S (X)h ♯ V (Y ).
Finally, we prove that the infinite product is preserved. Let X 0 , X 1 , . . .

⊆ A * . Then h ♯ V ( n≥0 X n ) = h V ( n≥0 X n ) = n≥0 h S (X n ) = n≥0 h S (X n ) = n≥0 h ♯ S (X n ).
It is clear that h S extends h, and that (h S , h V ) is unique.

Consider now (P (A * ), P (A ω )) with infinite product defined by n≥0 X n = {u 0 u 1 . . . ∈ A ω : u n ∈ X n , n ≥ 0}. It is also a continuous Kleene ω-algebra. Moreover, it satisfies 1 ω = ⊥. Lemma 3.4 (P (A * ), P (A ω )) is a quotient of (P (A * ), P (A ∞ )) under the continuous homomorphism (ϕ S , ϕ V ) such that ϕ S is the identity on P (A * ) and ϕ

V maps Y ⊆ A ∞ to Y ∩ A ω . Proof. Suppose that Y i ⊆ A ∞ for all i ∈ I. It holds ϕ V ( i∈I Y i ) = A ω ∩ i∈I Y i = i∈I (A ω ∩ Y i ) = i∈I ϕ V (Y i ). Let X ⊆ A * and Y ⊆ A ∞ . Then h V (XY ) = XY ∩ A ω = X(Y ∩ A ω ) = ϕ S (X)ϕ V (Y ). Finally, let X 0 , X 1 , . . . ⊆ A * . Then h V ( n≥0 X n ) = {u 0 u 1 . . . ∈ A ω : u n ∈ X n } = n≥0 h S (X n ). Lemma 3.5 Suppose that (S, V ) is a continuous Kleene ω-algebra satisfying 1 ω = ⊥. Let (h S , h V ) be a continuous homomorphism (P (A * ), P (A ∞ )) → (S, V ). Then (h S , h V ) factors through (ϕ S , ϕ V ). Proof. Define h ′ S = h S and h ′ V : P (A ω ) → V by h ′ V (Y ) = h V (Y ), for all Y ⊆ A ω . Then clearly h S = ϕ S h ′ S . Moreover, h V = ϕ V h ′ V , since for all Y ⊆ A ∞ , Y ϕ V h ′ V = (Y ∩ A ω )h V = (Y ∩A ω )h V ∨(Y ∩A * )h S 1 ω = (Y ∩A ω )h V ∨((Y ∩A * )1 ω )h V = ((Y ∩A ω )∪(Y ∩A * )1 ω )h V = Y h V .
Since (ϕ S , ϕ V ) and (h S , h V ) are homomorphisms. so is (h ′ S , h ′ V ). It is clear that h ′ V preserves all suprema.

Corollary 3.6 For each set A, (P (A * ), P (A ω )) is the free continuous Kleene ω-algebra satisfying 1 ω = ⊥, freely generated by A.

Proof. Suppose that (S, V ) is a continuous Kleene ω-algebra satisfying 1 ω = ⊥. Let h : A → S. By Theorem 3.3, there is a unique continuous homomorphism (h S , h V ) : (P (A * ), P (A ∞ )) → (S, V ) extending h. By Lemma 3.5, h S and h V factor as h S = ϕ S h ′ S and h

V = ϕ V h ′ V , where (h ′ S , h ′ V ) is a continuous homomorphism (P (A * ), P (A ω )) → (S, V ). This homomorphism (h ′ S , h ′ V )
is the required extension of h to a continuous homomorphism (P (A * ), P (A ω )) → (S, V ). Since the factorization is unique, so is this extension.

* -Continuous Kleene ω-algebras

In this section, we define * -continuous Kleene ω-algebras and finitary * -continuous Kleene ω-algebras as an extension of the * -continuous Kleene algebras of [START_REF] Kozen | On Kleene Algebras and Closed Semirings[END_REF]. We establish several basic properties of these structures, including the existence of the supremum of certain subsets including those corresponding to regular ω-languages.

We define a * -continuous Kleene ω-algebra (S, V ) as a * -continuous Kleene algebra (S, ∨, •, ⊥, 1, * ) acting on a (necessarily idempotent) semimodule V = (V, ∨, ⊥) subject to the usual laws of unitary action as well as the following axiom Ax0:

xy * v = n≥0 xy n v,
for all x, y ∈ S and v ∈ V . Moreover, there is an infinite product operation mapping an ω-sequence (x 0 , x 1 , . . .) (or ω-word x 0 x 1 . . .) over S to an element n≥0 x n of V . Thus, infinite product is a function S ω → V , where S ω denotes the set of all ω-sequences over S.

Infinite product is subject to the following axioms relating the infinite product to the other operations of Kleene ω-algebras and operations on ω-sequences. The first two axioms are the same as for continuous Kleene ω-algebras. The last two ones are weaker forms of the complete additivity of the infinite product of continuous Kleene ω-algebras.

Ax1: For all x 0 , x 1 , . . . ∈ S, n≥0 x n = x 0 n≥0 y n , where y n = x n+1 for all n ≥ 0.

Ax2: Suppose that x 0 , x 1 , . . . ∈ S and 0

= n 0 ≤ n 1 ≤ • • • is a sequence which increases without a bound. Let y k = x n k • • • x n k+1 -1 for all k ≥ 0. Then n≥0 x n = k≥0 y k .
Ax3: For all x 0 , x 1 , . . . and y, z in S, n≥0

x n (y ∨ z) =

x ′ n ∈{y,z} n≥0

x n x ′ n .

Ax4: Suppose that x, y 0 , y 1 , . . . are in S. Then n≥0

x * y n = kn≥0 n≥0

x kn y n .

It is clear that every continuous Kleene ω-algebra is * -continuous.

Some of our results will also hold for weaker structures. We define a finitary * -continuous Kleene ω-algebra as a structure (S, V ) as above, equipped with a star operation and an infinite product n≥0 x n restricted to finitary ω-sequences (or finitary ω-words) over S, i.e., to sequences x 0 , x 1 , . . . such that there is a finite subset F of S such that each x n is a finite product of elements of F . (Note that F is not fixed and may depend on the sequence x 0 , x 1 , . . . ) It is required that Ax1, Ax2 and Ax3 hold whenever the sequence x 0 , x 1 , . . . is finitary, and that Ax4 holds whenever the sequence y 0 , y 1 , . . . is finitary.

Finally, a generalized * -continuous Kleene algebra (S, V ) is defined as a * -continuous Kleene ω-algebra, but without the infinite product (and without Ax1-Ax4). However, it is assumed that Ax0 holds.

The above axioms have a number of consequences. For example, if x 0 , x 1 , . . . ∈ S and

x i = ⊥ for some i, then n≥0 x n = ⊥. Indeed, if x i = ⊥, then n≥0 x n = x 0 • • • x i n≥i+1 x n = ⊥ n≥i+1 x n = ⊥.
By Ax1 and Ax2, each * -continuous Kleene ω-algebra is an ω-semigroup, and equipped with the natural order relation, an ordered ω-semigroup, cf. [16, pp. 92f].

Similarly, when (S, V ) is a finitary * -continuous Kleene algebra and x 0 , x 1 , . . . is a finitary sequence over S, and if some x i is ⊥, then n≥0 x n = ⊥.

Suppose that (S, V ) is a * -continuous Kleene ω-algebra. To each word w ∈ S * there is a corresponding element w of S which is the product of the letters of w in the semiring S.

Similarly, when w ∈ S * V , there is an element w of V corresponding to w. Suppose now that a language X ⊆ S * or X ⊆ S * V . Then we can associate with X the set X = {w : w ∈ X}, which is a subset of S or V . The reader will probably be relieved that below we will denote w and X by just w and X, respectively,

The following facts are well-known (and follow from the result that the semirings of regular languages are the free * -continuous Kleene algebras [START_REF] Kozen | On Kleene Algebras and Closed Semirings[END_REF] (essentially shown also in [START_REF] Conway | Regular Algebra and Finite Machines[END_REF][START_REF] Salomaa | Two complete axiom systems for the algebra of regular events[END_REF]), and the free Kleene algebras [START_REF] Kozen | A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events[END_REF]).

(R 1 ∪ R 2 ) = R 1 ∨ R 2 (R 1 R 2 ) = ( R 1 )( R 2 ) (R * ) = ( R) * .
In a similar way, we can prove:

Lemma 4.3 Let (S, V ) be a generalized * -continuous Kleene-algebra. If R ⊆ S * is regular, x ∈ S and v ∈ V , then x( R)v = xRv. Proof. Suppose that R = ∅. Then x( R)v = ⊥ = xRv. If R is a singleton set {y}, then x( R)v = xyv = xRv. Suppose now that R = R 1 ∪ R 2 or R = R 1 R 2 ,
where R 1 , R 2 are regular, and suppose that our claim holds for

R 1 and R 2 . Then, if R = R 1 ∪ R 2 , x( R)v = x( R 1 ∨ R 2 )v (by Lemma 4.2) = x( R 1 )v ∨ x( R 2 )v = xR 1 v ∨ xR 2 v = x(R 1 ∪ R 2 )v = xRv,
where the third equality uses the induction hypothesis.

If R = R 1 R 2 , then x( R)v = x( R 1 )( R 2 )v (by Lemma 4.2) = (xR 1 ( R 2 )v) = {y( R 2 )v : y ∈ xR 1 } = { yR 2 v : y ∈ xR 1 } = xR 1 R 2 v = xRv,
where the second equality uses the induction hypothesis for R 1 and the fourth the one for R 2 . Suppose last that R = R * 0 , where R 0 is regular and our claim holds for R 0 . Then, using the previous case, it follows by induction that

x( R n 0 )v = xR n 0 v (1)
for all n ≥ 0. Using this and Ax0, it follows now that

x( R)v = x( R * 0 )y = x( n≥0 R n 0 )v = x( n≥0 ( R 0 ) n )v (by Lemma 4.2) = n≥0 x( R 0 ) n v (byAx0) = n≥0 x( R n 0 )v (by Lemma 4.2) = n≥0 xR n 0 v (by (1)) = xR * 0 v = xRv.
The proof is complete.

We can also prove:

Lemma 4.4 Let (S, V ) be a * -continuous Kleene ω-algebra. Suppose that the languages R 0 , R 1 , . . . ⊆ S * are regular and form a finite set R of languages. Moreover, let x 0 , x 1 , . . . ∈ S. Then

n≥0 x n ( R n ) = n≥0 x n R n .
Proof. If one of the R i is empty, our claim is clear since both sides are equal to ⊥, so we suppose they are all nonempty.

Below we will suppose that each regular language comes with a fixed decomposition having a minimal number of operations needed to obtain the language from the empty set and singleton sets. For a regular language R, let |R| denote the minimum number of operations needed to construct it. When R is a finite set of regular languages, let R ′ denote the set of non-singleton languages in it.

Let |R| = R∈R ′ 2 |R| . Our definition ensures that if R = {R, R 1 , . . . , R n } and R = R ′ ∪ R ′′ or R = R ′ R ′′ according to the fixed minimal decomposition of R, and if R ′ = {R ′ , R ′′ , R 1 , . . . , R n }, then |R ′ | < |R|. Similarly, if R = R * 0 by the fixed minimal decomposition and R ′ = {R 0 , R 1 , . . . , R n }, then |R ′ | < |R|.
We will argue by induction on |R|.

When |R| = 0, then R consists of singleton languages and our claim follows from Ax3. Suppose that |R| > 0. Let R be a non-singleton language appearing in R. If R appears only a finite number of times among the R n , then there is some

m such that R n is different from R for all n ≥ m. Then, n≥0 x n ( R n ) = i<m x i ( R i ) n≥m x n ( R n ) (by Ax1) = ( x 0 R 0 • • • x n-1 R n-1 ) n≥m x n ( R n ) (by Lemma 4.2) = (x 0 R 0 • • • x n-1 R n-1 n≥m x n ( R n )) (by Lemma 4.3) = {y n≥m x n ( R n ) : y ∈ x 0 R 0 • • • x n-1 R n-1 } = { y n≥m x n R n : y ∈ x 0 R 0 • • • x n-1 R n-1 } = n≥0 x n R n ,
where the passage from the 4th line to the 5th uses induction hypothesis and Ax1.

Suppose now that R appears an infinite number of times among the R n . Let R i 1 , R i 2 , . . . be all the occurrences of R among the R n . Define

y 0 = x 0 ( R 0 ) • • • ( R i 1 -1 )x i 1 y j = x i j +1 ( R i j +1 ) • • • ( R i j+1 -1 )x i j+1 , for j ≥ 1. Similarly, define Y 0 = x 0 R 0 • • • R i 1 -1 x i 1 Y j = x i j +1 R i j +1 • • • R i j+1 -1 x i j+1 ,
for all j ≥ 1. It follows from Lemma 4.2 that

y j = Y j for all j ≥ 0. Then n≥0 x n ( R n ) = j≥0 y j ( R), (2)
by Ax2, and n≥0

x n R n = j≥0 Y j R. If R = R ′ ∪ R ′′ , then: n≥0 x n ( R n ) = j≥0 y j ( (R ′ ∪ R ′′ )) (by (2)) = j≥0 y j ( R ′ ∨ R ′′ ) (by Lemma 4.2) = z j ∈{ R ′ , R ′′ } j≥0 y j z j (by Ax3) = z j ∈{ R ′ , R ′′ } j≥0 Y j z j = Z j ∈{R ′ ,R ′′ } j≥0 Y j Z j = n≥0 x n (R ′ ∪ R ′′ ) = n≥0 x n R,
where the 4th and 5th equalities hold by the induction hypothesis and Ax2.

Suppose now that R = R ′ R ′′ . Then applying the induction hypothesis almost directly we have

n≥0 x n ( R n ) = j≥0 y j ( R ′ R ′′ ) = j≥0 y j ( R ′ )( R ′′ ) (by Lemma 4.2) = j≥0 Y j ( R ′ )( R ′′ ) = j≥0 Y j R ′ R ′′ = n≥0 x n R ′ R ′′ = n≥0 x n R,
where the third and fourth equalities come from the induction hypothesis and Ax2.

The last case to consider is when R = T * , where T is regular. We argue as follows:

n≥0 x n ( R n ) = j≥0 y j ( T * ) = j≥0 y j ( T ) * (by Lemma 4.2) = k 0 ,k 1 ,... j≥0
y j ( T ) k j (by Ax1 and Ax4)

= k 0 ,k 1 ,... j≥0 Y j ( T ) k j = k 0 ,k 1 ,... j≥0 Y j T k j = j≥0 Y j T * = j≥0 Y j R j = n≥0 x n R n ,
where the 4th and 5th equalities follow from the induction hypothesis and Ax2. The proof is complete.

By the same proof, we have the following version of Lemma 4.4 for the finitary case:

Lemma 4.5 Let (S, V ) be a finitary * -continuous Kleene ω-algebra. Suppose that the languages R 0 , R 1 , • • • ⊆ S * are regular and form a finite set R of languages. Moreover, let x 0 , x 1 , . . . is a finitary sequence of elements of S. Then

n≥0 x n ( R n ) = n≥0 x n R n .
Note that each sequence x 0 , y 0 , x 1 , y 1 , . . . with y n ∈ R n is finitary.

As an immediate consequence of Lemma 4.5, we get the following result:

Corollary 4.6 Let (S, V ) be a finitary * -continuous Kleene ω-algebra. Suppose that R 0 , R 1 , . . . ⊆ S * are regular and form a finite set of languages. Then n≥0 R n exists and is equal to

n≥0 R n .
Suppose that (S, V ) is a * -continuous Kleene ω-algebra. When v = x 0 x 1 . . . ∈ S ω is an ωword over S, it naturally determines the element n≥0 x n of V . Thus, any subset X of S ω determines a subset of V . Using this convention, Lemma 4.4 may be rephrased as follows. For any * -continuous Kleene ω-algebra (S, V ), x 0 , x 1 , . . . ∈ S and regular sets R 0 , R 1 , . . . ⊆ S * that form a finite set, it holds that n≥0 x n ( R n ) = X where X ⊆ S ω is the set of all ω-words x 0 y 0 x 1 y 1 . . . with y i ∈ R i for all i ≥ 0, i.e., X = x 0 R 0 x 1 R 1 . . . Similarly, Corollary 4.6 asserts that if a subset of V corresponds to an infinite product over a finite collection of ordinary regular languages in S * , then the supremum of this set exists.

In any (finitary or non-finitary) * -continuous Kleene ω-algebra (S, V ), we define an ω-power operation S → V by x ω = n≥0 x for all x ∈ S. From the axioms we immediately have:

Corollary 4.7 Suppose that (S, V ) is a * -continuous Kleene ω-algebra or a finitary * -continuous Kleene ω-algebra. Then the following hold for all x, y ∈ S:

x ω = xx ω (xy) ω = x(yx) ω x ω = (x n ) ω , n ≥ 2.
Thus, each * -continuous Kleene ω-algebra gives rise to a Wilke algebra, even an ordered Wilke algebra [START_REF] Perrin | Infinite Words[END_REF][START_REF] Th | An Eilenberg theorem for infinity-languages[END_REF].

Lemma 4.8 Let (S, V ) be a * -continuous Kleene ω-algebra or a finitary * -continuous Kleene ω-algebra. Suppose that R ⊆ S ω is ω-regular. Then R exists in V .

Proof. It is well-known that R can be written as a finite union of sets of the form R 0 (R 1 ) ω where R 0 , R 1 ⊆ S * are regular, moreover, R 1 does not contain the empty word. It suffices to show that R 0 (R 1 ) ω exists. But this holds by Corollary 4.6.

Lemma 4.9 Let (S, V ) be a * -continuous Kleene ω-algebra. For all ω-regular sets R 1 , R 2 ⊆ S ω and regular sets R ⊆ S * it holds that

(R 1 ∪ R 2 ) = R 1 ∨ R 2 (RR 1 ) = ( R)( R 1 ).
And if R does not contain the empty word, then

R ω = ( R) ω .
Proof. The first claim is clear. The second follows from Lemma 4.3. For the last, see the proof of Lemma 4.8.

Free finitary * -continuous Kleene ω-algebras

Recall that for a set A, R(A * ) denotes the collection of all regular languages in A * . It is well-known that R(A * ), equipped with the usual operations, is a * -continuous Kleene algebra on A. Actually, R(A * ) is characterized up to isomorphism by the following universal property.

Call a function f : S → S ′ between * -continuous Kleene algebras a * -continuous homomorphism if it preserves all operations including star, so that it preserves the suprema of subsets of S of the form {x n : n ≥ 0}, where x ∈ S.

Theorem 5.1 [START_REF] Kozen | A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events[END_REF] For each set A, R(A * ) is the free * -continuous Kleene algebra, freely generated by A.

Thus, if S is any * -continuous Kleene algebra and h is any mapping of A into S, then h has a unique extension to a * -continuous Kleene algebra homomorphism h ♯ : R(A * ) → S.

Now let R ′ (A ∞ ) denote the collection of all subsets of A ∞ which are finite unions of sets of the form n≥0 R n , where each R n ⊆ A * is regular, and the set {R 0 , R 1 , . . .} is finite. Note that R ′ (A ∞ ) contains the empty set and is closed under finite unions. Moreover, when Y ∈ R ′ (A ∞ ) and u = a 0 a 1 . . . ∈ Y ∩ A ω , then the alphabet of u is finite, i.e., the set {a n : n ≥ 0} is finite.

Also, R ′ (A ∞ ) is closed under the action of R(A * ) inherited from (P (A * ), P (A ∞ )). The infinite product of a sequence of regular languages in R(A * ) is not necessarily contained in R ′ (A ∞ ), but by definition it contains all infinite products of finitary sequences over R(A * ).

Example 5.2 Let A = {a, b} and consider the set {aba 2 b . . . a n b . . .} containing a single ωword. It can be written as an infinite product of singleton subsets of A * , but it cannot be written as an infinite product R 0 R 1 . . . of regular languages in A * such that the set {R 0 , R 1 , . . .} is finite.

Proposition 5.3 (R(A * ), R ′ (A ∞ )) is a finitary * -continuous Kleene ω-algebra.
Proof. This is clear from the fact that (P (A * ), P (A ∞ )) is a continuous Kleene ω-algebra and that R(A * ) is a * -continuous semiring.

Theorem 5.4 (R(A * ), R ′ (A ∞ ))
is the free finitary * -continuous Kleene ω-algebra, freely generated by A.

Proof. Our proof is modeled after the proof of Theorem 3.3.

Suppose that (S, V ) is any finitary * -continuous Kleene ω-algebra and let h : A → S be a mapping. For each u = a 0 . . . a n-

1 in A * , define h S (u) = h(a 0 ) • • • h(a n-1 ) and h V (u) = h(a 0 ) • • • h(a n-1 )1 ω = k≥0 b k
, where b k = a k for all k < n and b k = 1 for all k ≥ n. When u = a 0 a 1 . . . ∈ A ω whose alphabet is finite, define h V (u) = k≥0 h(a k ). This infinite product exists in R ′ (A ∞ ).

Note that we have h S (uv) = h S (u)h S (v) for all u, v ∈ A * , and h S (ǫ) = 1. And if

u ∈ A * and v ∈ A ∞ such that the alphabet of v is finite, then h V (uv) = h S (u)h V (v). Also, h V (XY ) = h S (X)h V (Y ) for all X ⊆ A * in R(A * ) and Y ⊆ A ∞ in R ′ (A ∞ ).
Moreover, for all u 0 , u 1 , . . . in A * , if u i = ǫ for infinitely many i, such that the alphabet of

u 0 u 1 . . . is finite, then h V (u 0 u 1 . . .) = k≥0 h S (u k ). If on the other hand, u k = ǫ for all k ≥ n, then h V (u 0 u 1 . . .) = h S (u 0 ) • • • h S (u n-1 )1 ω .
In either case, if X 0 , X 1 , . . . ⊆ A * are regular and form a finitary sequence, then the sequence h S (X 0 ), h S (X 1 ), . . . is also finitary as is each infinite word in n≥0 X n , and

h V ( n≥0 X n ) = n≥0 h S (X n ). Suppose now that X ⊆ A * is regular and Y ⊆ A ∞ is in R ′ (A ∞ ). We define h ♯ S (X) = h S (X) and h ♯ V (Y ) = h V (Y ). It is well-known that h ♯ S is a * -continuous semiring morphism R(A * ) → S. Also, h ♯ V preserves finite suprema, since when I is finite, h ♯ V ( i∈I Y i ) = h V ( i∈I Y i ) = i∈I h V (Y i ) = i∈I h V (Y i ) = i∈I h ♯ V (Y i ).
We prove that the action is preserved.

Let X ∈ R(A * ) and Y ∈ R ′ (A ∞ ). Then h ♯ V (XY ) = h V (XY ) = h S (X)h V (Y ) = h S (X) h V (Y ) = h ♯ S (X)h ♯ V (Y ).
Finally, we prove that infinite product of finitary sequences is preserved. Let X 0 , X 1 , . . . be a finitary sequence of regular languages in R(A * ). Then, using Corollary 4.6, h

♯ V ( n≥0 X n ) = h V ( n≥0 X n ) = n≥0 h S (X n ) = n≥0 h S (X n ) = n≥0 h ♯ S (X n ).
It is clear that h S extends h, and that (h S , h V ) is unique.

Consider now (R(A * ), R ′ (A ω )) equipped with the infinite product operation n≥0 X n = {u 0 u 1 ∈ A ω : u n ∈ X n , n ≥ 0}, defined on finitary sequences X 0 , X 1 , . . . of languages in R ′ (A * ).

Proposition 5.5 (R(A * ), R ′ (A ω )) is a * continuous Kleene ω-algebra. Moreover, it satisfies 1 ω = ⊥. Lemma 5.6 (R(A * ), R ′ (A ω )) is a quotient of (R(A * ), R ′ (A ∞ )) under the * -continuous homo- morphism (ϕ S , ϕ V ) such that ϕ S is the identity function on P (A * ) and ϕ V maps Y ∈ R ′ (A ω ) to Y ∩ A ω . Lemma 5.7 Suppose that (S, V ) is a finitary * -continuous Kleene ω-algebra satisfying 1 ω = ⊥. Let (h S , h V ) be a * -continuous homomorphism (R(A * ), R ′ (A ∞ )) → (S, V ). Then (h S , h V ) factors through (ϕ S , ϕ V ).
Corollary 5.8 For each set A, (R(A * ), R ′ (A ω )) is the free finitary * -continuous Kleene ωalgebra satisfying 1 ω = ⊥, freely generated by A.

Proof. This follows from Theorem 5.4 using Lemma 5.7.

* -continuous Kleene ω-algebras and iteration semiring-semimodule pairs

In this section, our aim is to relate * -continuous Kleene ω-algebras to iteration semiringsemimodule pairs. Our main result will show that every (finitary or non-finitary) * -continuous Kleene ω-algebra is an iteration semiring-semimodule pair.

Some definitions are in order. Suppose that S is a semiring. Following [START_REF] Bloom | Iteration Theories -The Equational Logic of Iterative Processes[END_REF], we call S a Conway semiring if S is equipped with a star operation * : S → S satisfying

(x + y) * = (x * y) * x * (xy) * = 1 + x(yx) * y for all x, y ∈ S.
It is known that if S is a Conway semiring, then for each n ≥ 1, so is the semiring S n×n of all n × n-matrices over S with the usual sum and product operations and the star operation defined by induction on n so that if n > 1 and M = a b c d , where a and d are square matrices of dimension < n, then

M * = (a + bd * c) * (a + bd * c) * bd * (d + ca * b) * ca * (d + ca * b) * .
It is known that the above inductive definition does not depend on how M is split into 4 submatrices.

Suppose that S is a Conway semiring and G = {g 1 , . . . , g n } is a finite group of order n. For each x g 1 , . . . , x gn ∈ S, consider the n × n matrix M G = M G (x g 1 , . . . , x gn ) whose ith row is (x g -1 i g 1 , . . . , x g -1 i gn ), for i = 1, . . . , n, so that each row (and column) is a permutation of the first row. We say that the group identity [START_REF] Conway | Regular Algebra and Finite Machines[END_REF] associated with G holds in S if for each x g 1 , . . . , x gn , the first (and then any) row sum of M * G is (x g 1 + • • • + x gn ) * . Finally, we call S an iteration semiring [START_REF] Bloom | Iteration Theories -The Equational Logic of Iterative Processes[END_REF][START_REF] Ésik | Iteration semirings[END_REF] if all group identities hold in S.

Classes of examples of (idempotent) iteration semirings are given by the continuous Kleene algebras and the * -continuous Kleene algebras defined in the introduction. As mentioned above, the language semirings P (A * ) and the semirings P (A × A) of binary relations are continuous and hence also * -continuous Kleene algebras, and the semirings R(A * ) of regular languages are * -continuous Kleene algebras.

When S is a * -continuous Kleene algebra and n is a nonnegative integer, then the matrix semiring S n×n is also a * -continuous Kleene algebra and hence an iteration semiring, cf. [START_REF] Kozen | On Kleene Algebras and Closed Semirings[END_REF]. The star operation is defined by

M * i,j = m≥0, 1≤k 1 ,...,km≤n M i,k 1 M k 1 ,k 2 • • • M km,j ,
for all M ∈ S n×n and 1 ≤ i, j ≤ n. It is not immediately obvious to prove that the above supremum exists. The fact that M * is well-defined can be established by induction on n together with the well-known matrix star formula mentioned above: Suppose that n ≥ 2 and M = a b c d , where a and d are square matrices of dimension < n, then

M * = (a ∨ bd * c) * (a ∨ bd * c) * bd * (d ∨ ca * b) * ca * (d ∨ ca * b) * .
A semiring-semimodule pair (S, V ) is a Conway semiring-semimodule pair if it is equipped with a star operation * : S → S and an omega operation ω : S → V such that S is a Conway semiring and the following hold for all x, y ∈ S:

(x + y) ω = (x * y) * x ω + (x * y) ω (xy) ω = x(yx) ω .
It is known that when (S, V ) is a Conway semiring-semimodule pair, then so is (S n×n , V n ) for each n, where V n denotes the S n×n -semimodule of all n-dimensional (column) vectors over V with the action of S n×n defined similarly to matrix-vector product, and where the omega operation is defined by induction so that when n > 1 and M is the matrix a b c d , where a and d are square matrices of dimension < n, then

M ω = (a + bd * c) ω + (a + bd * c) * bd ω (d + ca * b) ω + (d + ca * b) * ca ω .
We also define iteration semiring-semimodule pairs [START_REF] Bloom | Iteration Theories -The Equational Logic of Iterative Processes[END_REF][START_REF] Ésik | On iteration semiring-semimodule pairs[END_REF] as those Conway semiring-semimodule pairs such that S is an iteration semiring and the omega operation satisfies the following condition: let M G = M G (x g 1 , . . . , x gn ) with x g 1 , . . . , x gn ∈ S for a finite group G = {g 1 , . . . , g n } of order n, then the first (and hence any) entry of M ω G is equal to (x

g 1 + • • • + x gn ) ω .
Examples of (idempotent) iteration semiring-semimodule pairs include the semiring-semimodule pairs (P (A * ), P (A ω )) of languages and ω-languages over an alphabet A, mentioned in the introduction. The omega operation is defined by X ω = n≥0 X n , where X n = X for all n ≥ 0. More generally, it is known that every continuous Kleene ω-algebra gives rise to an iteration semiring-semimodule pair. The omega operation is defined as for languages: x ω = n≥0 x n with x n = x for all n ≥ 0.

Other not necessarily idempotent examples include the complete and the (symmetric) biinductive semiring-semimodule pairs of [START_REF] Ésik | A semiring-semimodule generalization of ω-regular languages, Parts 1 and 2[END_REF][START_REF] Ésik | On iteration semiring-semimodule pairs[END_REF].

Suppose now that (S, V ) is a * -continuous Kleene ω-algebra. Then for each n ≥ 1, (S n×n , V n ) is a semiring-semimodule pair. The action of S n×n on V n is defined by a formula similar to matrix multiplication (viewing the elements of V n as column matrices). It is easy to see that (S n×n , V n ) is a generalized * -continuous Kleene algebra for each n ≥ 1.

Suppose that n ≥ 2. We would like to define an infinite product operation (S n×n ) ω → V n on matrices in S n×n by (

m≥0 M m ) i = 1≤i 1 ,i 2 ,...≤n (M 0 ) i,i 1 (M 1 ) i 1 ,i 2 • • •
for all 1 ≤ i ≤ n. However, unlike in the case of complete semiring-semimodule pairs [START_REF] Ésik | On iteration semiring-semimodule pairs[END_REF], the supremum on the right-hand side may not exist. Nevertheless it is possible to define an omega operation S n×n → V n and to turn (S n×n , V n ) into an iteration semiring-semimodule pair.

Lemma 6.1 Let (S, V ) be a (finitary) * -continuous Kleene ω-algebra. Suppose that M ∈ S n×n , where n ≥ 2. Then for every

1 ≤ i ≤ n, ( m≥0
M ) i = 1≤i 1 ,i 2 ,...≤n M i,i 1 M i 1 ,i 2 • • •
exists, so that we define M ω by the above equality.

Moreover, when M = a b c d , where a and d are square matrices of dimension < n, then

M ω = (a ∨ bd * c) ω ∨ (a ∨ bd * c) * bd ω (d ∨ ca * b) ω ∨ (d ∨ ca * b) * ca ω . (3)
Proof. Suppose that n = 2. Then by Corollary 4.6, (a ∨ bd * c) ω is the supremum of the set of all infinite products A 1,i 1 A i 1 ,i 2 • • • containing a or c infinitely often, and (a ∨ bd * c) * bd ω is the supremum of the set of all infinite products A 1,i 1 A i 1 ,i 2 • • • containing a and c only finitely often. Thus, (a ∨ bd * c) ω ∨ (a ∨ bd * c) * bd ω is the supremum of the set of all infinite products

A 1,i 1 A i 1 ,i 2 • • • . Similarly, (d ∨ ca * b) ω ∨ (d ∨ ca * b) * ca ω is the supremum of the set of all infinite products A 2,i 1 A i 1 ,i 2 • • • .
The proof of the induction step is similar. Suppose that n > 2, and let a be k × k. Then by induction hypothesis, for every i with 1 ≤ i ≤ k, the ith component of (a ∨ bd * c) ω is the supremum of the set of all infinite products A i,i 1 A i 1 ,i 2 • • • containing an entry of a or c infinitely often, whereas the ith component of (a ∨ bd * c) * bd ω is the supremum of all infinite products A i,i 1 A i 1 ,i 2 • • • containing entries of a and c only finitely often. Thus, the ith component of (a ∨ bd * c) ω ∨ (a ∨ bd * c) * bd ω is the supremum of the set of all infinite products A i,i

1 A i 1 ,i 2 • • • . A similar fact holds for (d ∨ ca * b) ω ∨ (d ∨ ca * b) * ca ω .
The proof is complete.

Theorem 6.2 Every (finitary) * -continuous Kleene ω-algebra is an iteration semiring-semimodule pair.

Proof. Suppose that (S, V ) is a finitary * -continuous Kleene ω-algebra. Then

(x ∨ y) ω = (x * y) ω ∨ (x * y) * x ω ,
since by Lemma 4.2 and Lemma 4.9, (x * y) ω is the supremum of the set of all infinite products over {x, y} containing y infinitely often, and (x * y) * x ω is the supremum of the set of infinite products over {x, y} containing y finitely often. Thus, (x * y) ω ∨ (x * y) * x ω is equal to (x ∨ y) ω , which by Ax3 is the supremum of all infinite products over {x, y}. As noted above, also

(xy) ω = x(yx) ω
for all x, y ∈ S. Thus, (S, V ) is a Conway semiring-semimodule pair and hence so is each (S n×n , V n ).

To complete the proof of the fact that (S, V ) is an iteration semiring-semimodule pair, suppose that x 1 , . . . , x n ∈ S, and let

x = x 1 ∨ • • • ∨ x n .
Let A be an n × n matrix whose rows are permutations of the x 1 , . . . , x n . We need to prove that each component of A ω is x ω . We use Lemma 6.1 and Ax3 to show that both are equal to the supremum of the set of all infinite products over the set X = {x 1 , . . . , x n }.

By Lemma 6.1, for each i 0 = 1, . . . , n, the i 0 th row of

A ω is i 1 ,i 2 ,... a i 0 ,i 1 a i 1 ,i 2 • • • . It is clear that each infinite product a i 0 ,i 1 a i 1 ,i 2 • • • is an infinite product over X. Suppose now that x j 0 x j 1 • • • is an infinite product over X.
We define by induction on k ≥ 0 an index i k+1 such that a i k ,i k+1 = x j k . Suppose that k = 0. Then let i 1 be such that a i 0 ,i 1 = x j 0 . Since x j 0 appears in the i 0 th row, there is such an i 1 . Suppose that k > 0 and that i k has already been defined. Since x j k appears in the i k th row, there is some i k+1 with a i k ,i k+1 = x j k . We have completed the proof of the fact that the i 0 th entry of A ω is the supremum of the set of all infinite products over the set X = {x 1 , . . . , x n }.

Consider now x ω = xx • • • . We use induction on n to prove that x ω is also the supremum of the set of all infinite products over the set X = {x 1 , . . . , x n }. When n = 1 this is clear. Suppose now that n > 0 and that the claim is true for n -1. Let y = x 1 ∨ • • • ∨ x n-1 so that x = y ∨ x n . We have:

x ω = (y ∨ x n ) ω = (x * n y) * x ω n ∨ (x * n y) ω = (x * n y) * x ω n ∨ (x * n x 1 ∨ • • • ∨ x * n x n-1 ) ω . Now (x * n y) * x ω n = k,m 1 ,...,m k ≥0 x m 1 n y • • • x m k n yx ω n ,
by Lemma 4.3, which is the supremum of all infinite products over X containing x 1 , . . . , x n-1 only a finite number of times.

Also, using the induction hypothesis and Ax4,

(x * n x 1 ∨ • • • ∨ x * n x n-1 ) ω = 1≤i 1 ,i 2 ,...≤n-1 x * n x i 1 x * n x i 2 • • • = 1≤i 1 ,i 2 ,...≤n-1 k 0 ,k 1 ,... x k 0 n x i 1 x k 1 n x i 2 • • •
which is the supremum of all infinite products over X containing one of x 1 , . . . , x n-1 an infinite number of times. Thus, x ω is the supremum of all infinite products over X as claimed. The proof is complete.

Relation to bi-inductive semiring-semimodule pairs

Recall that when P is a partially ordered set and f is a function P → P , then a pre-fixed point of f is an element x of P with xf ≤ x. Similarly, x ∈ P is a post-fixed point of f if x ≤ xf . Suppose that f is monotone and has x as its least pre-fixed point. Then x is a fixed point, i.e., xf = x, and thus the least fixed point of f . Similarly, when f is monotone, then the greatest post-fixed point of f , whenever it exists, is the greatest fixed point of f .

When S is a * -continuous Kleene algebra, then S is a Kleene algebra as defined in [START_REF] Kozen | On Kleene Algebras and Closed Semirings[END_REF]. Thus, for all x, y ∈ S, x * y is the least pre-fixed point (and thus the least fixed point) of the function S → S defined by z → xz ∨ y for all z ∈ S. Moreover, yx * is the least pre-fixed point and the least fixed point of the function S → S defined by z → zx ∨ y, for all z ∈ S.

Similarly, when (S, V ) is a generalized * -continuous Kleene algebra, then for all x ∈ S and v ∈ V , x * v is the least pre-fixed point and the least fixed point of the function V → V defined by z → xz ∨ v, where z ranges over V .

A bi-inductive semiring-semimodule pair is defined as a semiring-semimodule pair (S, V ) for which both S and V are partially ordered by the natural order relation ≤ such that the semiring and semimodule operations and the action are monotone, and which is equipped with a star operation * : S → S and an omega operation ω : S → V such that the following hold for all x, y ∈ S and v ∈ V :

• x * y is the least pre-fixed point of the function S → S mapping each z ∈ S to xz ∨ y,

• x * v is the least pre-fixed point of the function V → V mapping each z ∈ V to xz ∨ v, • x ω ∨ x * v is the greatest post-fixed point of the function V → V mapping each z ∈ V to xz ∨ v.
A bi-inductive semiring-semimodule pair is symmetric if for all x, y ∈ S, yx * is the least pre-fixed point of the functions S → S defined by z → zx + y for all z ∈ S.

By the above remarks we have:

Proposition 6.3 Suppose that (S, V ) is a finitary * -continuous Kleene ω-algebra. When for all x ∈ S and v ∈ V , x ω ∨ x * v is the greatest post-fixed point of the function V → V defined by z → xz ∨ v, then (S, V ) is a symmetric bi-inductive semiring-semimodule pair.
(It is known that every bi-inductive semiring-semimodule pair is an iteration semiring-semimodule pair, see [START_REF] Ésik | On iteration semiring-semimodule pairs[END_REF].)

7 Büchi automata in * -continuous Kleene ω-algebras

A generic definition of Büchi automata in Conway semiring-semimodule pairs was given in [START_REF] Bloom | Iteration Theories -The Equational Logic of Iterative Processes[END_REF][START_REF] Ésik | A semiring-semimodule generalization of ω-regular languages, Parts 1 and 2[END_REF]. In this section, we recall this general definition and apply it to (finitary) * -continuous Kleene ω-algebras. We give two different definitions of the behavior of a Büchi automaton, an algebraic and a combinatorial, and show that these two definitions are equivalent.

Suppose that (S, V ) is a Conway semiring-semimodule pair, S 0 is a subsemiring of S closed under star, and A is a subset of S. We write S 0 A to denote the set of all finite sums s 1 a 1 + • • • + s m a m with s i ∈ S 0 and a i ∈ A, for each i = 1, . . . , m.

We define a (weighted) Büchi automaton over (S 0 , A) of dimension n ≥ 1 in (S, V ) as a system A = (α, M, k) where α ∈ S 1×n 0 is the initial vector, M ∈ S 0 A n×n is the transition matrix, and k is an integer 0 ≤ k ≤ n. In order to define the behavior |A| of A, let us split M into 4 parts as above, M = a b c d , with a ∈ S 0 A k×k the top-left k-by-k submatrix. Then we define

|A| = α (a + bd * c) ω d * c(a + bd * c) ω .
We give another more combinatorial definition. A Büchi automaton A = (α, M, k) of dimension n may be represented as a transition system whose set of states is {1, . . . , n}. For any pair of states i, j, the transitions from i to j are determined by the (i, j)th entry M i,j of the transition matrix. Let M i,j = s 1 a 1 + • • • s m a m , say. Then either there are m transitions from i to j, respectively labeled s 1 a 1 , . . . , s n a n , or there is just one transition, whose label is M i,j . A run of the Büchi automaton starting in state i is an infinite path starting in state i which infinitely often visits at least one of the first k states, and the weight of such a run is the infinite product of the path labels. The behavior of the automaton in state i is the supremum of the weights of all runs starting in state i. Finally, the behavior of the automaton is α 1 w 1 + • • • + α n w n , where for each i, α i is the ith component of α and w i is the behavior in state i. Let |A| ′ denote the behavior of A according to this second definition. Proof. This holds by Lemma 6.1 and the fact that any matrix semiring over a * -continuous Kleene algebra is itself a * -continuous Kleene algebra.

For completeness we also mention a Kleene theorem for the Büchi automata introduced above, which is a direct consequence of the Kleene theorem for Conway semiring-semimodule pairs, cf. [START_REF] Ésik | A semiring-semimodule generalization of ω-regular languages, Parts 1 and 2[END_REF][START_REF] Ésik | Finite automata[END_REF]. Theorem 7.2 Suppose that (S, V ) is a * -continuous Kleene ω-algebra, S 0 is a subsemiring of S closed under star, and A ⊆ S. Then an element of V is the behavior of a Büchi automaton over (S 0 , V ) iff it is regular (or rational) over (S 0 , A), i.e., when it can be generated from the elements of S 0 ∪ A by the semiring and semimodule operations, the action, and the star and omega operations.

It is a routine matter to show that an element of V is rational over (S 0 , A) iff it can be written as n i=1 x i y ω i , where each x i and y i can be generated from S 0 ∪ A by , • and * .

Note that if f : L → L is a ⊤-continuous function which is different from the function ⊥, then ⊤f = ⊤.

Example 8.3 Suppose that L is a complete lattice and f : L → L is finitely additive and satisfies that for each x ∈ L, either xf n = ⊥ for some n ≥ 0, or xf = x, or n≥0 xf n = ⊤. Then f is locally finite. The functions id and ⊥ are locally finite and ⊤-continuous.

When L has at least two elements and ⊤ is the supremum of all elements different from ⊤, then the locally finite function f : L → L with xf = ⊥ for all x < ⊤ and ⊤f = ⊤ is not ⊤-continuous.

Lemma 8.4 Suppose that L is a complete lattice and f : L → L is finitely additive. Then the following conditions are equivalent.

• f is locally finite.

• For each x ∈ L, either n≥0 xf n = ⊤, or there is some n with x ∨ • • • ∨ xf n = x ∨ • • • ∨ xf n+1 . • For each x ∈ L, either n≥0 xf n = ⊤, or there is some n such that x ∨ • • • ∨ xf n = x ∨ • • • ∨ xf m for all m ≥ n. • For each x ∈ L, either n≥0 xf n = ⊤, or there is some n such that x ∨ • • • ∨ xf n = x ∨ • • • ∨ xf n ∨ xf m for all m ≥ n. Proof. Suppose that x ∈ L and xf * < ⊤, i.e., n≥0 xf n < ⊤. If f is locally finite then there is some n with xf * = x ∨ • • • ∨ xf n . Thus, for all m ≥ n, x ∨ • • • ∨ xf n ≤ x ∨ • • • xf n ∨ xf m ≤ x ∨ • • • ∨ xf m ≤ xf * = x ∨ • • • ∨ xf n . Also, if x∨• • •∨xf n = x∨• • •∨xf n+1 , then it follows by induction that x∨• • •∨xf n = x∨• • •∨xf m for all m ≥ n and thus xf * = x ∨ • • • ∨ xf n .
Indeed, this is clear when m = n, n + 1. Suppose that m > n + 1. Then, using the induction hypothesis and the fact that f is finitely additive,

x ∨ • • • ∨ xf m = x ∨ (x ∨ • • • ∨ xf m-1 )f = x ∨ (x ∨ • • • ∨ xf n )f = x ∨ • • • ∨ xf n+1 = x ∨ • • • ∨ xf n .
It is clear that the composition of ⊤-continuous functions is also ⊤-continuous. However, as the next example demonstrates, the composition of locally finite (and ⊤-continuous) functions is not necessarily locally finite.

Example 8.5 Let L be the following complete lattice (the linear sum of three infinite chains):

⊥ < x 0 < x 1 < • • • < y 0 < y 1 < • • • < z 0 < z 1 < • • • ⊤
Since L is a chain, a function L → L is finitely additive iff it is monotone and preserves ⊥.

Let f, g : L → L be the following functions. First, ⊥f = ⊥g = ⊥ and ⊤f = ⊤g = ⊤. Moreover, x i f = y i , y i f = z i g = ⊤ and x i g = ⊥, y i g = x i+1 , z i g = ⊤ for all i. Then f, g are monotone, uf * = u ∨ uf ∨ uf 2 and ug * = u ∨ ug for all u ∈ L. Also, f and g are ⊤-continuous, since if X = ⊤ then either ⊤ ∈ X or X ∩ {z 0 , z 1 , . . .} is infinite, but then Xf = Xg = ⊤. However, f g is not locally finite, since x 0 (f g)

* = x 0 ∨ x 0 (f g)∨ x 0 (f g) 2 • • • = x 0 ∨ x 1 ∨ x 2 ∨ • • • = y 0 .
We now show that if a set of locally finite and ⊤-continuous functions enjoys appropriate closure properties, then it is necessarily a * -continuous Kleene algebra.

Proposition 8.6 Suppose that S ⊆ FinAdd L is closed under the operations ∨, composition and star and contains the functions ⊥ and id. Moreover, suppose that each f ∈ S is locally finite and ⊤-continuous. Then S is a * -continuous Kleene algebra.

Proof. Suppose that g, h ∈ S. By Lemma 8.1, it suffices to show that g * h = n≥0 g n h. Since this is clear when h = ⊥, we assume that h is a function different from ⊥. Since g n h ≤ g * h for all n ≥ 0, it holds that n≥0 g n h ≤ g * h. To prove the opposite inequality, suppose that

x ∈ L. If xg * = ⊤, then n≥0 xg n = ⊤, so that n≥0 xg n h = ⊤ by ⊤-continuity. Thus, xg * h = ⊤ = n≥0 xg n h.
Suppose that xg * < ⊤. Then there is some m ≥ 0 with

xg * h = (x ∨ • • • ∨ xg m )h = xh ∨ • • • ∨ xg m h ≤ n≥0 xg n h = x( n≥0 g n h).
The proof is complete.

Next we study the closure properties of finitely additive ⊤-continuous functions in more detail. We will give a sufficient condition to the effect that the supremum of two such functions be also locally finite and ⊤-continuous. We will also prove that if f is locally finite and ⊤-continuous, then so is f * .

The following two propositions are also of independent interest. Proposition 8.7 Suppose that L is a complete lattice and f, g 1 , . . . , g k : L → L, k ≥ 0 are locally finite and ⊤-continuous functions. Then

f * g 1 • • • g k = n≥0 f n g 1 • • • g k .
Proof. When k = 0 this is obvious by definition of star, so we assume that k > 0. It is clear

that n≥0 f n g 1 • • • g k ≤ f * g 1 • • • g k in the pointwise order. To complete the proof, we show that xf * g 1 • • • g k ≤ n≥0 xf n g 1 • • • g k for all x ∈ L.
We may assume that the g i are different from the function ⊥ since in the opposite case

xf * g 1 • • • g k = ⊥.
Suppose first that xf * < ⊤. Then there is some n such that

xf * = x ∨ • • • ∨ xf n . Since the g i are finitely additive, it follows that xf * g 1 • • • g k = n i=0 xf i g 1 • • • g k ≤ n≥0 xf n g 1 • • • g k . Suppose next that xf * = ⊤, so that xf * g 1 • • • g k = ⊤. Our task is to prove that n≥0 xf n g 1 • • • g k = ⊤.
To this end, let h denote the function h = g 1 • • • g k . Since each g i is ⊤-continuous, so is h. Moreover, h is not the function ⊥. Thus, since {xf n : n ≥ 0} = ⊤ and h is ⊤-continuous,

n≥0 xf n g 1 • • • g k = n≥0 xf n h = ⊤.
Proposition 8.8 Suppose that L is a complete lattice and f, g ∈ FinAdd L such that f and f * g are locally finite and ⊤-continuous functions. Then

(f ∨ g) * = (f * g) * f * . Proof. It is clear that (f ∨g) n ≤ i≤n (f * g) i f * for all n ≥ 0, hence (f ∨g) * ≤ n≥0 (f * g) n f * ≤ (f * g) * f * . Below we will prove that (f * g) * f * ≤ n≥0 k i ≥0 f k 0 g • • • gf kn = (f ∨ g) * .
In our argument, we will make use of two observations. Claim 1. Suppose that x(f * g) n < ⊤ for some n ≥ 0. Then there exist integers k 1 , . . . , k n ≥ 0 with

x(f * g) n ≤ {xf i 1 g . . . f in g : i 1 ≤ k 1 , . . . , i n ≤ k n }.

Claim 2. Suppose that x(f * g) n f * < ⊤ for some n ≥ 0. Then there exist integers k 1 , . . . , k n , k n+1 ≥ 0 with

x(f * g) n f * ≤ {xf i 1 g . . . f in gf i n+1 : i 1 ≤ k 1 , . . . , i n+1 ≤ k n+1 }.
Since the proofs of these claims are similar, we only prove the first one. We argue by induction on n. When n = 0, our claim is clear. Suppose now that n > 0. Since x(f * g) n < ⊤ and

f * g preserves ⊤, x(f * g) n-1 = y < ⊤. Since f is locally finite, yf * = y ∨ • • • ∨ yf m for some m ≥ 0. Since g is finitely additive, yf * g = yg ∨ • • • ∨ yf m g. By the induction hypothesis, y ≤ {xf i 1 g . . . f i n-1 g : i 1 ≤ k 1 , . . . , i n-1 ≤ k n-1
} for some k 1 , . . . , k n-1 ≥ 0. Thus, using the fact that f and g are finitely additive, it follows that

x(f * g) n ≤ {xf i 1 g . . . f in g : i 1 ≤ k 1 , . . . , i n ≤ k n }
where k n = m.

We now return to the proof of the Proposition. Let x ∈ L. We want to show that x(f * g) * f * ≤ x(f ∨ g) * , which will follow if we can prove that x(f * g) * f * is the supremum of a finite or infinite number of elements of the form xf k 0 gf k 1 • • • gf kn where n ≥ 0 and k 0 , . . . , k n ≥ 0. Let us denote by ∆ x the set of all such elements.

When x = ⊤, then our claim is clear. So we may assume that x < ⊤. We consider several cases.

Case 1. x(f * g) * f * < ⊤. Then, since f * g is locally finite and f * is finitely additive,

x(f * g) * f * = (x ∨ • • • ∨ x(f * g) n )f * = xf * ∨ • • • ∨ x(f * g) n f *
for some n ≥ 0. Clearly, x(f * g) i < ⊤ and x(f * g) i f * < ⊤ for all i ≤ n. Now using Claim 2 and the fact that f is finitely additive, it follows that each x(f * g) i f * is the supremum of a finite number of terms of ∆ x .

Proof. We know that f ∨ g is finitely additive. By Proposition 8.8, (f ∨ g) * = (f * g) * f * .

Suppose that there is x ∈ L with x(f ∨ g) * = x(f * g) * f * < ⊤. Then, since f * g and f are locally finite and ⊤-continuous, we have that x(f * g)

* < ⊤, y = x(f * g) * = x ∨ • • • ∨ x(f * g) n ,
and yf * = y ∨ • • • ∨ yf m for some n, m ≥ 0. Moreover, as shown in the proof of Proposition 8.8, for each i ≤ n there exist n 1 , . . . , n i ≥ 0 with x(f * g) i = j 1 ≤n 1 ,...,j i ≤n i xf j 1 g . . . f j i g. It follows that x(f ∨ g) * = x ∨ • • • ∨ x(f ∨ g) k for some k ≥ 0. We have proved that f ∨ g is locally finite.

Since f and g are ⊤-continuous, f ∨ g is clearly also ⊤-continuous. Suppose that L, L ′ are complete lattices, and consider the collection FinAdd L,L ′ of all finitely additive functions L → L ′ , ordered pointwise. Then, as noted above, FinAdd L,L ′ is a complete lattice. Define a left action of FinAdd L on FinAdd L,L ′ by f v = f ; v, for all f ∈ FinAdd L and v ∈ FinAdd L,L ′ . It is a routine matter to check that FinAdd L,L ′ , equipped with the above action, the binary supremum operation ∨ and the constant ⊥ is an (idempotent) left FinAdd L -semimodule.

We extend the notion of ⊤-continuous functions L → L over a complete lattice to a more general situation in a natural way. Suppose that L and L ′ are complete lattices and let f : L → L ′ . We call f ⊤-continuous if f is finitely additive and Xf = ⊤ whenever X ⊆ L with X = ⊤.

We will make use of a general fact which is similar to Lemma 8.1.

Lemma 8.11 Suppose that L, L ′ are complete lattices, S is a * -continuous Kleene algebra in FinAdd L , and V ⊆ FinAdd L,L ′ is an S-semimodule. Then (S, V ) is a generalized *continuous Kleene algebra iff for all g ∈ S and v ∈ V , g * v = n≥0 g n v (and thus n≥0 g n v ∈ V ).

Proof. The above condition yields that for all f, g ∈ S and v ∈ V , f g * v = n≥0 f g n v, so that Ax0 holds. Proposition 8.12 Let S be a * -continuous Kleene algebra of locally finite and ⊤-continuous functions in FinAdd L , and let V be a subsemimodule of FinAdd L,L ′ closed under the induced S-action, which contains only ⊤-continuous functions. Then (S, V ) is a generalized * -continuous Kleene algebra.

Proof. The proof is similar to that of Proposition 8.6.

Remark 8.13 Actually it suffices to require in the above proposition the following. For all v ∈ V , v = ⊥, and for all f ∈ S and x ∈ L, if xf * = ⊤ then n≥0 xf n v = ⊤. Then (S, V ) is a generalized * -continuous Kleene algebra. Indeed, suppose that f ∈ S and v ∈ V . In order to prove that f

* v = n≥0 f n v, it suffices to show that xf * v ≤ n≥0 xf n v for all x. If xf * < ⊤, then xf * = x ∨ • • • ∨ xf n for some n. Since v is finitely additive, xf * v = xv ∨ • • • ∨ xf n v ≤ n≥0 xf n v. If xf * = ⊤, then xf * v = ⊤ unless v is ⊥. It follows that f * v = n≥0 f n v.
9 * -continuous Kleene ω-algebras of locally finite and ⊤-continuous functions

In this section, our aim is to study * -continuous Kleene ω-algebras of finitely additive functions.

For this reason, we define an infinite product mapping ω-sequences of finitely additive functions over a complete lattice into the 2-element lattice 2.

In this section, let L be an arbitrary complete lattice and let L ′ = 2, the 2-element lattice {⊥, ⊤}. Our aim is to study generalized * -continuous Kleene ω-algebras (S, V ), where S consists of locally finite ⊤-continuous functions L → L and V consists of ⊤-continuous functions L → 2.

For each sequence f

0 , f 1 , . . . ∈ FinAdd L , define g = n≥0 f n : L → 2 by xg = ⊥ iff there is an index n ≥ 0 for which xf 0 • • • f n = ⊥. Thus, if x, xf 0 , xf 0 f 1 , . . . are all different from ⊥, then x n≥0 f n = ⊤, otherwise x n≥0 f n = ⊥.
Note that in the latter case the sequence x, xf 0 , xf 0 f 1 , . . . is eventually ⊥.

It is easy to see that n≥0 f n is also finitely additive. Indeed, ⊥ n≥0 f n = ⊥ clearly holds, and for all x, y ∈ L, if x ≤ y in L, then x n≥0 f n ≤ y n≥0 f n . Thus, to prove that for all x, y ∈ L, it holds that ( for all k ≥ 0, so that each g k is also finitely additive. Then

x ∨ y) n≥0 f n = x n≥0 f n ∨ y n≥0 f n , it suffices to show that if x n≥0 f n = y n≥0 f n = ⊥, then (x ∨ y) n≥0 f n = ⊥. But if x n≥0 f n = y n≥0 f n = ⊥, then there exist m, k with xf 0 • • • f m = yf 0 • • • f k = ⊥. Let ℓ = max{m, k}. We have that (x ∨ y)f 0 • • • f ℓ = xf 0 • • • f ℓ ∨ yf 0 • • • f ℓ = ⊥,
n≥0 f n = f 0 n≥0 f n+1 n≥0 f n = k≥0 g k .
Proposition 9.2 The following property holds for all finitely additive functions f 0 , f 1 , . . . and g 0 , g 1 , . . . L → L:

n≥0 (f n ∨ g n ) =
hn∈{fn,gn} n≥0

h n . (4)
In particular, Ax3 holds.

Proof. Suppose that f 0 , g 0 , f 1 , g 1 , . . . are in FinAdd L . Since infinite product is monotone, the term on the right-hand side of (4) is less than or equal to the term on the left-hand side.

To prove that equality holds, let x ∈ L and suppose that x n≥0 (f n ∨ g n ) = ⊤. It suffices to Lemma 9.6 Suppose that L is a complete lattice for which it holds that whenever X = ⊤ for some X ⊆ L, then for all x < ⊤ in L there is y ∈ X with x ≤ y. If f 0 , f 1 , . . . is a sequence of locally finite ⊤-continuous functions L → L, then n≥0 f n is ⊤-continuous.

Proof. Let v = n≥0 f n . We already know that v is finitely additive. We need to show that if v = ⊥, then v is ⊤-continuous. But if v = ⊥, then there is some x < ⊤ with xv = ⊤, i.e., such that xf 0 • • • f n > ⊥ for all n. By assumption, there is some y ∈ X with x ≤ y. It follows that yf 0 • • • f n ≥ xf 0 • • • f n > ⊥ for all n and thus Xv = ⊤.

Fixed points

In this short section, we relate * -continuous Kleene ω-algebras of locally finite and ⊤-continuous functions to bi-inductive semiring-semimodule pairs. Lemma 9.7 Suppose that L is a complete lattice and (S, V ) is a generalized * -continuous Kleene algebra of locally finite ⊤-continuous functions L → L and ⊤-continuous functions L → 2. Suppose that for each f ∈ S, f ω = n≥0 f ∈ V . Then for all f ∈ S and v ∈ V , f ω ∨ f * v is the greatest post-fixed point of the map V → V given by z → f z ∨ v.

Proof. Since f f ω = f ω , we have that f

(f ω ∨ f * v) ∨ v = f f ω ∨ f f * v ∨ v = f ω ∨ f * v.
Suppose that u ∈ V with u ≤ f u ∨ v. Then u ≤ f n u ∨ f n-1 v ∨ • • • ∨ v for all n ≥ 0. We want to show that xu ≤ xf ω ∨ xf * v for all x ∈ L. This is clear when xf ω = ⊤. So suppose that xf ω = ⊥. Then xf n = ⊥ for some n. Thus,

xu ≤ xf n-1 v ∨ • • • xv ≤ xf * v = xf ω ∨ xf * v.
Corollary 9.8 Suppose that L is a complete lattice and (S, V ) is a generalized * -continuous Kleene algebra of locally finite ⊤-continuous functions L → L and ⊤-continuous functions L → 2. Suppose that for each f ∈ S, f ω = n≥0 f ∈ V . Then (S, V ) is a symmetric bi-inductive semiring-semimodule pair.

10 Application: Energy Problems

We finish the paper by showing how the setting developed in the last two sections can be applied to solve so-called energy problems. We refer to [START_REF] Ésik | Kleene algebras and semimodules for Energy Problems[END_REF] for a more detailed account of, and motivation for, energy problems in the context of formal modeling and verification.

Let L = [0, ⊤] ⊥ be the complete lattice of nonnegative real numbers together with ⊤ = ∞ and an extra bottom element ⊥, and extend the usual order and operations on real numbers to [0, ⊤] ⊥ by declaring that ⊥ < x < ⊤, ⊥x = ⊥ and ⊤ + x = ⊤ for all nonnegative reals x.

Note that L satisfies the condition required in Lemma 9.6: If X ⊆ [0, ⊤] ⊥ is such that X = ⊤, then for all x ∈ L with x < ⊤ there is y ∈ X for which x ≤ y.

An energy function is a mapping f : [0, ⊤] ⊥ → [0, ⊤] ⊥ for which ⊥f = ⊥, ⊤f = ⊥ if xf = ⊥ for all x < ⊤ and ⊤f = ⊤ otherwise, and yf ≥ xf + yx whenever ⊥ < x < y < ⊤. The set of such functions is denoted E.

Theorem 10.6 A final state in A is reachable with initial energy x ∈ [0, ⊤] ⊥ iff xαM * ζ > ⊥.

There is an infinite run in A from initial energy x which visits an accepting state infinitely often iff xα|A| = ⊤.

Conclusion

We have introduced continuous and (finitary and non-finitary) * -continuous Kleene ω-algebras and exposed some of their basic properties. Continuous Kleene ω-algebras are idempotent complete semiring-semimodule pairs, and conceptually, * -continuous Kleene ω-algebras are a generalization of continuous Kleene ω-algebras in much the same way as * -continuous Kleene algebras are of continuous Kleene algebras: In * -continuous Kleene algebras, suprema of finite sets and of sets of powers are required to exist and to be preserved by the product; in * -continuous Kleene ω-algebras these suprema are also required to be preserved by the infinite product.

It is known that in a Kleene algebra, * -continuity is precisely what is required to be able to compute the reachability value of a weighted automaton (or its power series) using the matrix star operation. Similarly, we have shown that the Büchi values of automata over * -continuous ω-algebras can be computed using the matrix omega operation.

We have seen that the sets of finite and infinite languages over an alphabet are the free continuous Kleene ω-algebras, and that the free finitary * -continuous Kleene ω-algebras are given by the sets of regular languages and of finite unions of finitary infinite products of regular languages. A characterization of the free (non-finitary) * -continuous Kleene ω-algebras (and whether they even exist) is left open.

Lemma 4 . 1 Lemma 4 . 2

 4142 Suppose that S is a * -continuous Kleene algebra. If R ⊆ S * is regular, then R exists. Moreover, for all x, y ∈ S, x( R)y = xRy. Let S be a * -continuous Kleene-algebra. Suppose that R, R 1 and R 2 are regular subsets of S * . Then

Theorem 7 . 1

 71 For every Büchi automaton A over (S 0 , A) in a finitary * -continuous Kleene ω-algebra, it holds that |A| = |A| ′ .

8. 1

 1 Generalized * -continuous Kleene algebras of finitely additive functions By the previous results, locally finite and ⊤-continuous functions provide examples of *continuous Kleene algebras. Next we show that they also yield generalized * -continuous Kleene algebras.

Proposition 9 . 1

 91 and thus (x ∨ y) n≥0 f n = ⊥.It is clear that Ax1 and Ax2 hold. Suppose that f 0 , f 1 , . . . are finitely additive functions L → L and 0= n 0 ≤ n 1 ≤ • • • is a sequence of integers which increases without a bound. Let g k = f n k • • • f n k+1 -1

* The first author acknowledges partial support by grant no. K108448 from the National Foundation of Hungary for Scientific Research. The second and third authors acknowledge partial support by ANR MALTHY, grant no. ANR-13-INSE-0003 from the French National Research Foundation.

We have shown that other examples of * -continuous Kleene ω-algebras are given by locally finite and ⊤-continuous functions over complete lattices. We have seen that every * -continuous Kleene ω-algebra is an iteration semiring-semimodule pair, which permits to compute the behavior of Büchi automata with weights in a * -continuous Kleene ω-algebra using ω-powers of matrices. Hence the algebraic setting developed here can be employed to solve energy problems for hybrid systems.

8 * -continuous (generalized) Kleene algebras of locally finite and ⊤-continuous functions

In the following two sections our aim is to provide additional examples of * -continuous Kleene ω-algebras. These examples are motivated by energy problems for hybrid systems and stem from [START_REF] Ésik | Kleene algebras and semimodules for Energy Problems[END_REF]. We will deal with a generalization of the notion of energy function used in [START_REF] Ésik | Kleene algebras and semimodules for Energy Problems[END_REF].

In this section, we define locally finite and ⊤-continuous functions over complete lattices and show that they give rise to (generalized) * -continuous Kleene algebras.

Suppose that L = (L, ≤) is a complete lattice with bottom and top elements ⊥ and ⊤. Then a finitely additive function over L is a function f : L → L with ⊥f = ⊥ and (x ∨ y)f = xf ∨ yf for all x, y ∈ L. (We write function application and composition in the diagrammatic order, from left to write.) In the same way, one may define finitely additive functions L → L ′ for complete lattices L, L ′ . Note that when f : L → L ′ is finitely additive, then ( X)f = Xf for all finite sets ⊆ L.

Consider the collection FinAdd L,L ′ of all finitely additive functions f : L → L ′ , ordered pointwise. Since the (pointwise) supremum of any set of finitely additive functions is finitely additive, FinAdd L,L ′ is also a complete lattice, in which the supremum of any set of functions can be constructed pointwise. The least and greatest elements are the constant functions with value ⊥ and ⊤, respectively. By an abuse of notation, we will denote these functions by ⊥ and ⊤ as well.

Suppose now that L = L ′ , so that we just write FinAdd L . Since the composition of finitely additive functions is finitely additive and the identity function id over L is finitely additive, and since composition of finitely additive functions distributes over finite suprema, FinAdd L , equipped with the operation ∨ (binary supremum), ; (composition), and the constant function ⊥ and the identity function id as 1, is an idempotent semiring. It follows that when f is finitely additive, then so is f * = n≥0 f n . Moreover, f ≤ f * and f * ≤ g * whenever f ≤ g. Below we will usually write just f g for the composition f ; g.

All functions between complete lattices considered in this paper will be (at least) finitely additive.

Lemma 8.1 Let L be a complete lattice and S be any subsemiring of FinAdd L closed under the star operation. Then S is a * -continuous Kleene algebra iff for all g, h ∈ S, g * h = n≥0 g n h.

Proof. Suppose that the above condition holds. We need to show that

by assumption, and we conclude that f ( n≥0 g n h) = n≥0 f g n h since the supremum is pointwise.

Definition 8.2 Let L be a complete lattice and f : L → L a finitely additive function. We call f locally finite if for each x ∈ L,

Within this case, we consider sub-cases.

Sub-case 2.1. x(f * g) * < ⊤. In this case, it follows as in Case 1 using Claim

Then, as shown above, for each n ≥ 0 we can write i≤n (f * g) i as a finite supremum of elements of ∆ x . Thus, x(f * g) * f * = ⊤ = x(f * g) * is a possibly infinite supremum of elements of ∆ x . Suppose now that there is some n with i≤n (f * g) i = ⊤. Then there is a least such n.

Let us denote it by n 0 . Since

Last, assume that x(f * g) n 0 = ⊤. Let us denote x(f * g) n 0 -1 by y, so that y < ⊤ and yf * g = ⊤.

Note that y is a finite supremum of elements of ∆ x .

Suppose that yf

Since f is finitely additive, each yf i is a finite supremum over ∆ x , and we conclude that so is

and by finite additivity, we conclude that yf * g is a finite supremum of elements of ∆ x .

Next we prove that the star of a locally finite ⊤-continuous function also has these properties.

Lemma 8.9 Suppose that L is a complete lattice and f ∈ FinAdd L is locally finite. Then f * is also locally finite. And if f is additionally ⊤-continuous, then so is f * .

Proof. Suppose that f is locally finite. We prove that xf

By finite additivity, it follows that Suppose now that f is additionally ⊤-continuous. We need to show is that f * is also ⊤continuous. To this end, let X ⊆ L with X = ⊤. Since x ≤ xf * , for all x ∈ X, it holds that Xf * ≥ X = ⊤. Thus Xf * = ⊤.

Lemma 8.10 Suppose that L is a complete lattice and f, g, f * g : L → L are locally finite ⊤-continuous functions. Then f ∨ g is also locally finite and ⊤-continuous.

show that there is a choice of the functions h n ∈ {f n , g n } such that x n≥0 h n = ⊤. Consider the full (ordered) binary tree where each node at level n ≥ 0 is the source of an edge labeled f n and an edge labeled g n , ordered as indicated. We can assign to each node u the composition h u of the functions that occur as the labels of the edges along the unique path from the root to that node. Let us mark a node u if xh u = ⊥. Since x n≥0 (f n ∨ g n ) = ⊤, each level contains a marked node. Moreover, whenever a node is marked and has a predecessor, its predecessor is also marked. By König's lemma there is an infinite path going through marked nodes. This infinite path gives rise to the sequence h 0 , h 1 , . . . with x n≥0 h n = ⊤.

Proposition 9.3 Suppose that f, g 0 , g 1 , . . . are locally finite and ⊤-continuous functions L → L. Then n≥0 f * g n = k 0 ,k 1 ,...≥0 n≥0 f kn g n , i.e., Ax4 holds.

Proof. Since f is locally finite and ⊤-continuous, so is f * , by Lemma 8.9. Let x ∈ L. Suppose that x n≥0 f * g n = ⊤. We want to prove that there exist integers k 0 , k 1 , . . . such that x n≥0 f kn g n = ⊤. Consider the ordered infinite binary tree and label the left out-edge of each vertex v by f and the right out-edge by g n iff the unique path from the root to v contains exactly n right out-edges. To each vertex z we can canonically associate the function h z which is the composition of the edge labels that occur along the path from the root to z. Let us mark a vertex z if following condition holds: if z 1 , . . . , z k are some ancestors of z such that each z i+1 is the left successor of z i , for i < k, then it is not the case that

Since x n≥0 f * g n = ⊤, for each n there is a marked vertex which is the target of an edge labeled g n . Moreover, any ancestor of a marked vertex is marked. By König's lemma, there is an infinite path going through marked vertices. If this path contains infinitely many right edges, we are done, since this infinite path determines the integers k n , n ≥ 0. Indeed, the edge labels of the path form an infinite word

Suppose the path contains only a finite number of right edges. For simplicity, we may as well assume that the path contains only left edges. This means that x, xf, xf 2 , . . . satisfy that for all n, xf n ≤ i<n xf i and thus xf * = ⊤, since f is locally finite and ⊤-continuous. Since none of the functions g 0 , g 1 , . . .

Thus, xf m v = ⊥ for some m. We may thus choose k 0 = m and k n = 0 for all n > 0.

Corollary 9.4 Suppose that L is a complete lattice and (S, V ) is a generalized * -continuous Kleene algebra of locally finite and ⊤-continuous functions L → L and ⊤-continuous functions L → 2. Suppose that n≥0 f n ∈ V for all sequences f 0 , f 1 , . . . of functions in S. Then (S, V ) is a * -continuous Kleene ω-algebra.

Corollary 9.5 Suppose that L is a complete lattice and (S, V ) is a generalized * -continuous Kleene algebra of locally finite and ⊤-continuous functions L → L and ⊤-continuous functions L → 2. Suppose that n≥0 f n ∈ V for all finitary sequences f 0 , f 1 , . . . of functions in S. Then (S, V ) is a finitary * -continuous Kleene ω-algebra.

Suppose that L is a complete lattice and f 0 , f 1 , . . . is a sequence of locally finite ⊤-continuous functions L → L, and consider the function v = n≥0 f n : L → 2 defined above. While v is finitely additive, it may not be ⊤-continuous. Below we provide a sufficient condition under which this function is also ⊤-continuous.

The above entails that for all f ∈ E and all x < y ∈ [0, ⊤] ⊥ , xf = ⊤ implies yf = ⊤ and yf = ⊥ implies xf = ⊥. Note that energy functions are monotone, hence finitely additive, and that E is closed under (pointwise) binary supremum ∨ and composition.

Lemma 10.1 Energy functions are ⊤-continuous.

Proof. Let X ⊆ [0, ⊤] ⊥ such that X = ⊤ and f ∈ E, f = ⊥. We have X = {⊥}, so let x 0 ∈ X \ {⊥} and, for all n ≥ 0, x n = x 0 + n. Let y n = x n f . If y n = ⊥ for all n ≥ 0, then also nf = ⊥ for all n ≥ 0 (as x n ≥ n), hence f = ⊥. We must thus have an index N for which y N > ⊥. But then y N +k ≥ y N + k for all k ≥ 0, hence Xf = ⊤.

Hence f is locally finite and f * ∈ E.

Proof. We have ⊥f * = ⊥ and ⊤f

We can now apply Proposition 8.6: By Proposition 8.12, (E, V) is a generalized * -continuous Kleene algebra. We can now apply Corollaries 9.4 and 9.8:

Corollary 10.5 (E, V) is a * -continuous Kleene ω-algebra and a symmetric bi-inductive semiringsemimodule pair.

The paper [START_REF] Ésik | Kleene algebras and semimodules for Energy Problems[END_REF] is concerned with reachability and Büchi acceptance in so-called energy automata, which are finite automata labeled with energy functions. This is useful for solving certain energy and resource management problems in real-time and hybrid systems, see [START_REF] Ésik | Kleene algebras and semimodules for Energy Problems[END_REF] for details.

Let A = (α, M, k) be an energy automaton of dimension n ≥ 1, with α ∈ {⊥, id} 1×n ⊆ E 1×n , M ∈ E E n×n and 0 ≤ k ≤ n as in Section 7 (hence S 0 = A = E in the notation of that section). Define ζ ∈ {⊥, id} n×1 by ζ i = id if i ≤ k, ζ i = ⊥ for i > k. We can now apply the results of this paper to conclude the following: