-
Formal Translation from Reversing Petri Nets to Coloured Petri Nets
Authors:
Kamila Barylska,
Anna Gogolinska,
Lukasz Mikulski,
Anna Philippou,
Marcin Piatkowski,
Kyriaki Psara
Abstract:
Reversible computation is an emerging computing paradigm that allows any sequence of operations to be executed in reverse order at any point during computation. Its appeal lies in its potential for lowpower computation and its relevance to a wide array of applications such as chemical reactions, quantum computation, robotics, and distributed systems. Reversing Petri nets are a recently-proposed ex…
▽ More
Reversible computation is an emerging computing paradigm that allows any sequence of operations to be executed in reverse order at any point during computation. Its appeal lies in its potential for lowpower computation and its relevance to a wide array of applications such as chemical reactions, quantum computation, robotics, and distributed systems. Reversing Petri nets are a recently-proposed extension of Petri nets that implements the three main forms of reversibility, namely, backtracking, causal reversing, and out-of-causal-order reversing. Their distinguishing feature is the use of named tokens that can be combined together to form bonds. Named tokens along with a history function, constitute the means of remembering past behaviour, thus, enabling reversal. In recent work, we have proposed a structural translation from a subclass of RPNs to the model of Coloured Petri Nets (CPNs), an extension of traditional Petri nets where tokens carry data values. In this paper, we extend the translation to handle RPNs with token multiplicity under the individual-token interpretation, a model which allows multiple tokens of the same type to exist in a system. To support the three types of reversibility, tokens are associated with their causal history and, while tokens of the same type are equally eligible to fire a transition when going forward, when going backwards they are able to reverse only the transitions they have previously fired. The new translation, in addition to lifting the restriction on token uniqueness, presents a refined approach for transforming RPNs to CPNs through a unifying approach that allows instantiating each of the three types of reversibility. The paper also reports on a tool that implements this translation, paving the way for automated translations and analysis of reversible systems using CPN Tools.
△ Less
Submitted 1 November, 2023;
originally announced November 2023.
-
Token Multiplicity in Reversing Petri Nets Under the Individual Token Interpretation
Authors:
Anna Philippou,
Kyriaki Psara
Abstract:
Reversing Petri nets (RPNs) have recently been proposed as a net-basedapproach to model causal and out-of-causal order reversibility. They are based on the notion of individual tokens that can be connected together via bonds. In this paper we extend RPNs by allowing multiple tokens of the same type to exist within a net based on the individual token interpretation of Petri nets. According to this…
▽ More
Reversing Petri nets (RPNs) have recently been proposed as a net-basedapproach to model causal and out-of-causal order reversibility. They are based on the notion of individual tokens that can be connected together via bonds. In this paper we extend RPNs by allowing multiple tokens of the same type to exist within a net based on the individual token interpretation of Petri nets. According to this interpretation, tokens of the same type are distinguished via their causal path. We develop a causal semantics of the model and we prove that the expressive power of RPNs with multiple tokens is equivalent to that of RPNs with single tokens by establishing an isomporphism between the Labelled Transition Systems (LTSs) capturing the reachable parts of the respective RPN models.
△ Less
Submitted 6 September, 2022;
originally announced September 2022.
-
Reversible Computation in Cyclic Petri Nets
Authors:
Anna Philippou,
Kyriaki Psara
Abstract:
Petri nets are a mathematical language for modeling and reasoning about distributed systems. In this paper we propose an approach to Petri nets for embedding reversibility, i.e., the ability of reversing an executed sequence of operations at any point during operation. Specifically, we introduce machinery and associated semantics to support the three main forms of reversibility namely, backtrackin…
▽ More
Petri nets are a mathematical language for modeling and reasoning about distributed systems. In this paper we propose an approach to Petri nets for embedding reversibility, i.e., the ability of reversing an executed sequence of operations at any point during operation. Specifically, we introduce machinery and associated semantics to support the three main forms of reversibility namely, backtracking, causal reversing, and out-of-causal-order reversing in a variation of cyclic Petri nets where tokens are persistent and are distinguished from each other by an identity. Our formalism is influenced by applications in biochemistry but the methodology can be applied to a wide range of problems that feature reversibility. In particular, we demonstrate the applicability of our approach with a model of the ERK signalling pathway, an example that inherently features reversible behavior.
△ Less
Submitted 7 October, 2020;
originally announced October 2020.
-
Controlling Reversibility in Reversing Petri Nets with Application to Wireless Communications
Authors:
Anna Philippou,
Kyriaki Psara,
Harun Siljak
Abstract:
Petri nets are a formalism for modelling and reasoning about the behaviour of distributed systems. Recently, a reversible approach to Petri nets, Reversing Petri Nets (RPN), has been proposed, allowing transitions to be reversed spontaneously in or out of causal order. In this work we propose an approach for controlling the reversal of actions of an RPN, by associating transitions with conditions…
▽ More
Petri nets are a formalism for modelling and reasoning about the behaviour of distributed systems. Recently, a reversible approach to Petri nets, Reversing Petri Nets (RPN), has been proposed, allowing transitions to be reversed spontaneously in or out of causal order. In this work we propose an approach for controlling the reversal of actions of an RPN, by associating transitions with conditions whose satisfaction/violation allows the execution of transitions in the forward/reversed direction, respectively. We illustrate the framework with a model of a novel, distributed algorithm for antenna selection in distributed antenna arrays.
△ Less
Submitted 28 May, 2019;
originally announced May 2019.
-
Distributed Antenna Selection for Massive MIMO using Reversing Petri Nets
Authors:
Harun Siljak,
Kyriaki Psara,
Anna Philippou
Abstract:
Distributed antenna selection for Distributed Massive MIMO (Multiple Input Multiple Output) communication systems reduces computational complexity compared to centralised approaches, and provides high fault tolerance while retaining diversity and spatial multiplexity. We propose a novel distributed algorithm for antenna selection and show its advantage over existing centralised and distributed sol…
▽ More
Distributed antenna selection for Distributed Massive MIMO (Multiple Input Multiple Output) communication systems reduces computational complexity compared to centralised approaches, and provides high fault tolerance while retaining diversity and spatial multiplexity. We propose a novel distributed algorithm for antenna selection and show its advantage over existing centralised and distributed solutions. The proposed algorithm is shown to perform well with imperfect channel state information, and to execute a small number of simple computational operations per node, converging fast to a steady state. We base it on Reversing Petri Nets, a variant of Petri nets inspired by reversible computation, capable of both forward and backward execution while obeying conservation laws.
△ Less
Submitted 28 May, 2019;
originally announced May 2019.
-
Fault Adaptive Routing in Metasurface Controller Networks
Authors:
Taqwa Saeed,
Constantinos Skitsas,
Dimitrios Kouzapas,
Marios Lestas,
Vassos Soteriou,
Anna Philippou,
Sergi Abadal,
Christos Liaskos,
Loukas Petrou,
Julius Georgiou,
Andreas Pitsillides
Abstract:
HyperSurfaces are a merge of structurally reconfigurable metasurfaces whose electromagnetic properties can be changed via a software interface, using an embedded miniaturized network of controllers, thus enabling novel capabilities in wireless communications. Resource constraints associated with the development of a hardware testbed of this breakthrough technology necessitate network controller ar…
▽ More
HyperSurfaces are a merge of structurally reconfigurable metasurfaces whose electromagnetic properties can be changed via a software interface, using an embedded miniaturized network of controllers, thus enabling novel capabilities in wireless communications. Resource constraints associated with the development of a hardware testbed of this breakthrough technology necessitate network controller architectures different from traditional regular Network-on-Chip architectures. The Manhattan-like topology chosen to realize the controller network in the testbed under development is irregular, with restricted local path selection options, operating in an asynchronous fashion. These characteristics render traditional fault-tolerant routing mechanisms inadequate. In this paper, we present work in progress towards the development of fault-tolerant routing mechanisms for the chosen architecture. We present two XY-based approaches which have been developed aiming to offer reliable data delivery in the presence of faults. The first approach aims to avoid loops while the second one attempts to maximize the success delivery probabilities. Their effectiveness is demonstrated via simulations conducted on a custom developed simulator.
△ Less
Submitted 15 October, 2018;
originally announced October 2018.
-
Formal Verification of a Programmable Hypersurface
Authors:
Panagiotis Kouvaros,
Dimitris Kouzapas,
Anna Philippou,
Julius Georgiou,
Loukas Petrou,
Andreas Pitsillides
Abstract:
A metasurface is a surface that consists of artificial material, called metamaterial, with configurable electromagnetic properties. This paper presents work in progress on the design and formal verification of a programmable metasurface, the Hypersurface, as part of the requirements of the VISORSURF research program (HORIZON 2020 FET-OPEN). The Hypersurface design is concerned with the development…
▽ More
A metasurface is a surface that consists of artificial material, called metamaterial, with configurable electromagnetic properties. This paper presents work in progress on the design and formal verification of a programmable metasurface, the Hypersurface, as part of the requirements of the VISORSURF research program (HORIZON 2020 FET-OPEN). The Hypersurface design is concerned with the development of a network of switch controllers that are responsible for configuring the metamaterial. The design of the Hypersurface, however, has demanding requirements that need to be delivered within a context of limited resources. This paper shares the experience of a rigorous design procedure for the Hypersurface network, that involves iterations between designing a network and its protocols and the formal evaluation of each design. Formal evaluation has provided results that, so far, drive the development team in a more robust design and overall aid in reducing the cost of the Hypersurface manufacturing. This paper presents work in progress on the design and formal verification of a programmable Hypersurface as part of the requirements of the VISORSURF research programme (HORIZON 2020 FET-OPEN).
△ Less
Submitted 17 July, 2018;
originally announced July 2018.
-
Reversible Computation in Petri Nets
Authors:
Anna Philippou,
Kyriaki Psara
Abstract:
Reversible computation is an unconventional form of computing where any executed sequence of operations can be executed in reverse at any point during computation. It has recently been attracting increasing attention in various research communities as on the one hand it promises low-power computation and on the other hand it is inherent or of interest in a variety of applications. In this paper, w…
▽ More
Reversible computation is an unconventional form of computing where any executed sequence of operations can be executed in reverse at any point during computation. It has recently been attracting increasing attention in various research communities as on the one hand it promises low-power computation and on the other hand it is inherent or of interest in a variety of applications. In this paper, we propose a reversible approach to Petri nets by introducing machinery and associated operational semantics to tackle the challenges of the three main forms of reversibility, namely, backtracking, causal reversing and out-of-causal-order reversing. Our proposal concerns a variation of Petri nets where tokens are persistent and are distinguished from each other by an identity which allows for transitions to be reversed spontaneously in or out of causal order. Our design decisions are influenced by applications in biochemistry but the methodology can be applied to a wide range of problems that feature reversibility. In particular, to demonstrate the applicability of our approach we use an example of a biochemical system and an example of a transaction-processing system both of which naturally embed reversible behaviour.
△ Less
Submitted 10 April, 2018;
originally announced April 2018.
-
Process Ordering in a Process Calculus for Spatially-Explicit Ecological Models
Authors:
Anna Philippou,
Mauricio Toro
Abstract:
In this paper we extend PALPS, a process calculus proposed for the spatially-explicit individual-based modeling of ecological systems, with the notion of a policy. A policy is an entity for specifying orderings between the different activities within a system. It is defined externally to a PALPS model as a partial order which prescribes the precedence order between the activities of the individu-…
▽ More
In this paper we extend PALPS, a process calculus proposed for the spatially-explicit individual-based modeling of ecological systems, with the notion of a policy. A policy is an entity for specifying orderings between the different activities within a system. It is defined externally to a PALPS model as a partial order which prescribes the precedence order between the activities of the individu- als of which the model is comprised. The motivation for introducing policies is twofold: one the one hand, policies can help to reduce the state-space of a model, on the other hand, they are useful for exploring the behavior of an ecosystem under different assumptions on the ordering of events within the system. To take account of policies, we refine the semantics of PALPS via a transition relation which prunes away executions that do not respect the defined policy. Furthermore, we propose a translation of PALPS into the probabilistic model checker PRISM . We illustrate our framework by applying PRISM on PALPS models with policies for conducting simulation and reachability analysis.
△ Less
Submitted 4 March, 2018;
originally announced March 2018.
-
Privacy by ty** in the $π$-calculus
Authors:
Dimitrios Kouzapas,
Anna Philippou
Abstract:
In this paper we propose a formal framework for studying privacy in information systems. The proposal follows a two-axes schema where the first axis considers privacy as a taxonomy of rights and the second axis involves the ways an information system stores and manipulates information. We develop a correspondence between the above schema and an associated model of computation. In particular, we pr…
▽ More
In this paper we propose a formal framework for studying privacy in information systems. The proposal follows a two-axes schema where the first axis considers privacy as a taxonomy of rights and the second axis involves the ways an information system stores and manipulates information. We develop a correspondence between the above schema and an associated model of computation. In particular, we propose the \Pcalc, a calculus based on the $π$-calculus with groups extended with constructs for reasoning about private data. The privacy requirements of an information system are captured via a privacy policy language. The correspondence between the privacy model and the \Pcalc semantics is established using a type system for the calculus and a satisfiability definition between types and privacy policies. We deploy a type preservation theorem to show that a system respects a policy and it is safe if the ty** of the system satisfies the policy. We illustrate our methodology via analysis of two use cases: a privacy-aware scheme for electronic traffic pricing and a privacy-preserving technique for speed-limit enforcement.
△ Less
Submitted 17 December, 2017; v1 submitted 17 October, 2017;
originally announced October 2017.
-
Mean-Field Semantics for a Process Calculus for Spatially-Explicit Ecological Models
Authors:
Mauricio Toro,
Anna Philippou,
Sair Arboleda,
María Puerta,
Carlos M. Vélez S.
Abstract:
We define a mean-field semantics for S-PALPS, a process calculus for spatially-explicit, individual-based modeling of ecological systems. The new semantics of S-PALPS allows an interpretation of the average behavior of a system as a set of recurrence equations. Recurrence equations are a useful approximation when dealing with a large number of individuals, as it is the case in epidemiological st…
▽ More
We define a mean-field semantics for S-PALPS, a process calculus for spatially-explicit, individual-based modeling of ecological systems. The new semantics of S-PALPS allows an interpretation of the average behavior of a system as a set of recurrence equations. Recurrence equations are a useful approximation when dealing with a large number of individuals, as it is the case in epidemiological studies. As a case study, we compute a set of recurrence equations capturing the dynamics of an individual-based model of the transmission of dengue in Bello (Antioquia), Colombia.
△ Less
Submitted 3 March, 2016;
originally announced March 2016.
-
A Process Calculus for Spatially-explicit Ecological Models
Authors:
Margarita Antonaki,
Anna Philippou
Abstract:
We propose PALPS, a Process Algebra with Locations for Population Systems. PALPS allows us to produce spatially-explicit, individual-based models and to reason about their behavior. Our calculus has two levels: at the first level we may define the behavior of an individual of a population while, at the second level, we may specify a system as the collection of individuals of various species locate…
▽ More
We propose PALPS, a Process Algebra with Locations for Population Systems. PALPS allows us to produce spatially-explicit, individual-based models and to reason about their behavior. Our calculus has two levels: at the first level we may define the behavior of an individual of a population while, at the second level, we may specify a system as the collection of individuals of various species located in space, moving through their life cycle while changing their location, if they so wish, and interacting with each other in various ways such as preying on each other. Furthermore, we propose a probabilistic temporal logic for reasoning about the behavior of PALPS processes. We illustrate our framework via models of dispersal in metapopulations.
△ Less
Submitted 17 November, 2012;
originally announced November 2012.
