-
High Altitude Platform Stations: the New Network Energy Efficiency Enabler in the 6G Era
Authors:
Tailai Song,
David Lopez,
Michela Meo,
Nicola Piovesan,
Daniela Renga
Abstract:
The rapidly evolving communication landscape, with the advent of 6G technology, brings new challenges to the design and operation of wireless networks. One of the key concerns is the energy efficiency of the Radio Access Network (RAN), as the exponential growth in wireless traffic demands increasingly higher energy consumption. In this paper, we assess the potential of integrating a High Altitude…
▽ More
The rapidly evolving communication landscape, with the advent of 6G technology, brings new challenges to the design and operation of wireless networks. One of the key concerns is the energy efficiency of the Radio Access Network (RAN), as the exponential growth in wireless traffic demands increasingly higher energy consumption. In this paper, we assess the potential of integrating a High Altitude Platform Station (HAPS) to improve the energy efficiency of a RAN, and quantify the potential energy conservation through meticulously designed simulations. We propose a quantitative framework based on real traffic patterns to estimate the energy consumption of the HAPS integrated RAN and compare it with the conventional terrestrial RAN. Our simulation results elucidate that HAPS can significantly reduce energy consumption by up to almost 30\% by exploiting the unique advantages of HAPS, such as its self-sustainability, high altitude, and wide coverage. We further analyze the impact of different system parameters on performance, and provide insights for the design and optimization of future 6G networks. Our work sheds light on the potential of HAPS integrated RAN to mitigate the energy challenges in the 6G era, and contributes to the sustainable development of wireless communications.
△ Less
Submitted 3 July, 2023;
originally announced July 2023.
-
An Interleaving Semantics of the Timed Concurrent Language for Argumentation to Model Debates and Dialogue Games
Authors:
Stefano Bistarelli,
Maria Chiara Meo,
Carlo Taticchi
Abstract:
Time is a crucial factor in modelling dynamic behaviours of intelligent agents: activities have a determined temporal duration in a real-world environment, and previous actions influence agents' behaviour. In this paper, we propose a language for modelling concurrent interaction between agents that also allows the specification of temporal intervals in which particular actions occur. Such a langua…
▽ More
Time is a crucial factor in modelling dynamic behaviours of intelligent agents: activities have a determined temporal duration in a real-world environment, and previous actions influence agents' behaviour. In this paper, we propose a language for modelling concurrent interaction between agents that also allows the specification of temporal intervals in which particular actions occur. Such a language exploits a timed version of Abstract Argumentation Frameworks to realise a shared memory used by the agents to communicate and reason on the acceptability of their beliefs with respect to a given time interval. An interleaving model on a single processor is used for basic computation steps, with maximum parallelism for time elapsing. Following this approach, only one of the enabled agents is executed at each moment. To demonstrate the capabilities of language, we also show how it can be used to model interactions such as debates and dialogue games taking place between intelligent agents. Lastly, we present an implementation of the language that can be accessed via a web interface. Under consideration in Theory and Practice of Logic Programming (TPLP).
△ Less
Submitted 7 July, 2023; v1 submitted 13 June, 2023;
originally announced June 2023.
-
Verification of Time-Aware Business Processes using Constrained Horn Clauses
Authors:
Emanuele De Angelis,
Fabio Fioravanti,
Maria Chiara Meo,
Alberto Pettorossi,
Maurizio Proietti
Abstract:
We present a method for verifying properties of time-aware business processes, that is, business process where time constraints on the activities are explicitly taken into account. Business processes are specified using an extension of the Business Process Modeling Notation (BPMN) and durations are defined by constraints over integer numbers. The definition of the operational semantics is given by…
▽ More
We present a method for verifying properties of time-aware business processes, that is, business process where time constraints on the activities are explicitly taken into account. Business processes are specified using an extension of the Business Process Modeling Notation (BPMN) and durations are defined by constraints over integer numbers. The definition of the operational semantics is given by a set OpSem of constrained Horn clauses (CHCs). Our verification method consists of two steps. (Step 1) We specialize OpSem with respect to a given business process and a given temporal property to be verified, whereby getting a set of CHCs whose satisfiability is equivalent to the validity of the given property. (Step 2) We use state-of-the-art solvers for CHCs to check the satisfiability of such sets of clauses. We have implemented our verification method using the VeriMAP transformation system, and the Eldarica and Z3 solvers for CHCs.
△ Less
Submitted 9 August, 2016;
originally announced August 2016.
-
Timed Soft Concurrent Constraint Programs: An Interleaved and a Parallel Approach
Authors:
Stefano Bistarelli,
Maurizio Gabbrielli,
Maria Chiara Meo,
Francesco Santini
Abstract:
We propose a timed and soft extension of Concurrent Constraint Programming. The time extension is based on the hypothesis of bounded asynchrony: the computation takes a bounded period of time and is measured by a discrete global clock. Action prefixing is then considered as the syntactic marker which distinguishes a time instant from the next one. Supported by soft constraints instead of crisp one…
▽ More
We propose a timed and soft extension of Concurrent Constraint Programming. The time extension is based on the hypothesis of bounded asynchrony: the computation takes a bounded period of time and is measured by a discrete global clock. Action prefixing is then considered as the syntactic marker which distinguishes a time instant from the next one. Supported by soft constraints instead of crisp ones, tell and ask agents are now equipped with a preference (or consistency) threshold which is used to determine their success or suspension. In the paper we provide a language to describe the agents behavior, together with its operational and denotational semantics, for which we also prove the compositionality and correctness properties. After presenting a semantics using maximal parallelism of actions, we also describe a version for their interleaving on a single processor (with maximal parallelism for time elapsing). Coordinating agents that need to take decisions both on preference values and time events may benefit from this language. To appear in Theory and Practice of Logic Programming (TPLP).
△ Less
Submitted 22 April, 2014; v1 submitted 24 February, 2014;
originally announced March 2014.
-
Unfolding for CHR programs
Authors:
Maurizio Gabbrielli,
Maria Chiara Meo,
Paolo Tacchella,
Herbert Wiklicky
Abstract:
Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption, and more generally to optimize a given program. Essentially, it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. Unfolding is one of the basic operations which is used by most program transformation systems and which consists i…
▽ More
Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption, and more generally to optimize a given program. Essentially, it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. Unfolding is one of the basic operations which is used by most program transformation systems and which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages.
This paper defines an unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning. We also prove that, under some suitable conditions, confluence and termination are preserved by the above transformation.
To appear in Theory and Practice of Logic Programming (TPLP)
△ Less
Submitted 2 July, 2013;
originally announced July 2013.
-
Decidability properties for fragments of CHR
Authors:
Maurizio Gabbrielli abd Jacopo Mauro,
Maria Chiara Meo,
Jon Sneyers
Abstract:
We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity >0). Both languages allow the use of the = built-in in the body of rules, thus are built on a host language that supports unification. However each imposes one further restriction. The first CHR dialect allows…
▽ More
We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity >0). Both languages allow the use of the = built-in in the body of rules, thus are built on a host language that supports unification. However each imposes one further restriction. The first CHR dialect allows only range-restricted rules, that is, it does not allow the use of variables in the body or in the guard of a rule if they do not appear in the head. We show that the existence of an infinite computation is decidable for this dialect. The second dialect instead limits the number of atoms in the head of rules to one. We prove that in this case, the existence of a terminating computation is decidable. These results show that both dialects are strictly less expressive than Turing Machines. It is worth noting that the language (without function symbols) without these restrictions is as expressive as Turing Machines.
△ Less
Submitted 26 July, 2010;
originally announced July 2010.
-
Unfolding in CHR
Authors:
Maurizio Gabbrielli,
Maria Chiara Meo,
Paolo Tacchella
Abstract:
Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption and more generally to optimize a given program. Essentially it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. One of the basic operations which is used by most program transformation systems is unfolding which consists in th…
▽ More
Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption and more generally to optimize a given program. Essentially it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. One of the basic operations which is used by most program transformation systems is unfolding which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages and, to the best of our knowledge, no other has considered unfolding of CHR programs.
This paper defines a correct unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning. We prove that confluence and termination properties are preserved by the above transformations.
△ Less
Submitted 25 July, 2008;
originally announced July 2008.
-
On the Expressive Power of Multiple Heads in CHR
Authors:
Cinzia Di Giusto,
Maurizio Gabbrielli,
Maria Chiara Meo
Abstract:
Constraint Handling Rules (CHR) is a committed-choice declarative language which has been originally designed for writing constraint solvers and which is nowadays a general purpose language. CHR programs consist of multi-headed guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached. Many empirical evidences suggest that multiple heads augment the expressi…
▽ More
Constraint Handling Rules (CHR) is a committed-choice declarative language which has been originally designed for writing constraint solvers and which is nowadays a general purpose language. CHR programs consist of multi-headed guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached. Many empirical evidences suggest that multiple heads augment the expressive power of the language, however no formal result in this direction has been proved, so far.
In the first part of this paper we analyze the Turing completeness of CHR with respect to the underneath constraint theory. We prove that if the constraint theory is powerful enough then restricting to single head rules does not affect the Turing completeness of the language. On the other hand, differently from the case of the multi-headed language, the single head CHR language is not Turing powerful when the underlying signature (for the constraint theory) does not contain function symbols.
In the second part we prove that, no matter which constraint theory is considered, under some reasonable assumptions it is not possible to encode the CHR language (with multi-headed rules) into a single headed language while preserving the semantics of the programs. We also show that, under some stronger assumptions, considering an increasing number of atoms in the head of a rule augments the expressive power of the language.
These results provide a formal proof for the claim that multiple heads augment the expressive power of the CHR language.
△ Less
Submitted 18 January, 2011; v1 submitted 21 April, 2008;
originally announced April 2008.
-
A compositional Semantics for CHR
Authors:
Maurizio Gabbrielli,
Maria Chiara Meo
Abstract:
Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a solved form is reached.
CHR has received a considerable attention, both from the practical and from the theoretical side. Nevertheless, due the us…
▽ More
Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a solved form is reached.
CHR has received a considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multi-headed clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far.
In this paper we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools.
△ Less
Submitted 20 March, 2006;
originally announced March 2006.
-
Proving correctness of Timed Concurrent Constraint Programs
Authors:
F. S. de Boer,
M. Gabbrielli,
M. C. Meo
Abstract:
A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior…
▽ More
A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior of timed concurrent constraint programs.
△ Less
Submitted 28 August, 2002;
originally announced August 2002.
-
Transformations of CCP programs
Authors:
Sandro Etalle,
Maurizio Gabbrielli,
Maria Chiara Meo
Abstract:
We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations which guarantee that the input/output CCP semantics is preserved also when distinguishing deadlocked computations from successful ones and when considering intermediate results of (possibly) non-terminating computations.
The system allows us to o…
▽ More
We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations which guarantee that the input/output CCP semantics is preserved also when distinguishing deadlocked computations from successful ones and when considering intermediate results of (possibly) non-terminating computations.
The system allows us to optimize CCP programs while preserving their intended meaning: In addition to the usual benefits that one has for sequential declarative languages, the transformation of concurrent programs can also lead to the elimination of communication channels and of synchronization points, to the transformation of non-deterministic computations into deterministic ones, and to the crucial saving of computational space. Furthermore, since the transformation system preserves the deadlock behavior of programs, it can be used for proving deadlock freeness of a given program wrt a class of queries. To this aim it is sometimes sufficient to apply our transformations and to specialize the resulting program wrt the given queries in such a way that the obtained program is trivially deadlock free.
△ Less
Submitted 10 July, 2001;
originally announced July 2001.
