We explore the abstractness of semantic models for concurrent languages designed using continuation-passing style. By employing techniques from metric semantics and continuations for concurrency, we establish a formal relationship between denotational semantics and operational semantics for a concurrent language based on Hoare's CSP. We extend CSP by introducing a mechanism for communication and synchronization across multiple channels, which supports multiparty synchronous interactions among an arbitrarily large (finite) number of concurrent processes. We demonstrate that the denotational semantics is weakly abstract w.r.t. the corresponding operational semantics.

We investigate the abstractness of a continuation semantics for a calculus inspired by DNA computing. This semantic investigation is given in the framework of complete metric spaces, and uses the weak abstractness criterion introduced by us in recent work. We prove that the denotational semantics designed with continuations is weakly abstract with respect to the operational semantics of our calculus which involves multiparty synchronization. We show that the expected concurrency laws are satisfied in this semantics for the calculus under investigation.

In recent works we have introduced the quantitative programming paradigm which provides a framework for the formal verification of concurrent programs. By partitioning the set of program states into bisimulation equivalence classes, this paradigm enables the formal verification of concurrent programs with large state spaces. For formal verification, (as in our previous works) we employ probabilistic model checking techniques. To enable formal verification, the programmer must bound the ranges of variables, and programs are translated into corresponding finite state probabilistic models. In this paper we introduce new constructions for quantitative programming that enable the programmer to maintain the compliance between the program under verification and the corresponding probabilistic model, taking into consideration the execution rates of program statements. For formal verification we use continuous-time Markov chains and a notion of strong bisimulation specific to stochastic process algebras. We present formal verification experiments performed using PRISM probabilistic model checker.

This article presents the Haskell implementations of spiking neural P systems and of two variants subsequently introduced in the literature, namely the spiking neural P systems with inhibitory rules and spiking neural P systems with structural plasticity. These implementations are obtained using their operational semantics in which the involved configurations use continuations. For each variant, the formal syntax is presented, together with the semantics given accurately by the Haskell implementation.

Quantitative programming (or performance evaluation programming) is a programming paradigm, which supports the formal verification of (bounded versions of) concurrent programs by using model checking techniques. By partitioning the state space of programs into bisimulation equivalence classes, this approach enables the formal verification of programs with large state spaces. The paradigm was introduced by us in previous works by developing an experimental concurrent language designed to facilitate the construction of probabilistic models that capture the behavior of programs and that can be verified by using probabilistic model checking techniques. The experimental language introduced in previous works is extended in this paper with constructions which enable the specification of behavioral equivalence classes. Concurrent programs are translated into corresponding probabilistic models, which are analyzed by using the PRISM probabilistic model checker. The programmer identifies bisimulation equivalence classes to enable the formal verification of programs with large state spaces. For formal verification, we employ Markov Decision Processes.

This paper presents a calculus inspired by the spiking neural P systems. Its operational and denotational semantics are defined; they are related by using the metric semantics methodology, showing that the denotational semantics is correct with respect to the operational one. We use the continuations for concurrency to describe precisely the nondeterministic behaviour, the time delays between firings and spikings, as well as the synchronized functioning specific to spiking neural P systems. (c) 2022 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons.org/licenses/ by/4.0/).

We use the functional programming language Haskell to design semantic interpreters for the spiking neural P systems. Haskell provides an appropriate support for implementing the denotational semantics of a concurrent language inspired by the spiking neural P systems. This language and its semantics describe properly the structure and behaviour of the spiking neural P systems. The semantic interpreters capture accurately the nondeterministic behaviour, the time delays between firings and spikings, and the synchronization specific to spiking neural P systems.

In recent work we have introduced performance evaluation programming - a programming paradigm supporting performance analysis and formal verification of concurrent programs. For software verification the ranges of variables must be bounded, and programs are translated into finite-state continuous-time Markov chains verified formally by using probabilistic model checking techniques. Our present aim is to increase the size of the state space of programs that can be verified formally. The solution investigated in this paper is inspired by equivalence partitioning - a well-known software testing technique. We provide experimental results showing that, by partitioning the state space of concurrent programs into behavioral equivalence classes, the performance evaluation programming paradigm can be used to design and verify formally concurrent programs with large state spaces.

We present an operational semantics designed in continuation-passing style for an abstract concurrent language providing a general mechanism of multiparty interactions. Using the classic notion of strong bisimulation, we show that the basic laws of concurrent systems are satisfied in this semantics. By customizing the behavior of continuations, we obtain semantic models for formalisms based on Milner’s CCS extended with constructions for multiparty interactions.

We present a semantic domain for designing concurrent languages in continuation-passing style (CPS). We offer denotational semantics designed in CPS for languages based on Milner’s CCS extended with mechanisms which support multiparty interactions. We establish a collection of properties which can describe the behavior of concurrent systems with multiparty interactions. The semantic investigation is accomplished in the mathematical framework of complete metric spaces.

We employ the mathematical methodology of metric semantics in designing the continuation-based denotational and operational semantics for two process calculi recently investigated in the literature based on well-known Milner's CCS. We prove that our denotational models are weakly abstract with respect to their corresponding operational models.

We present a metric denotational semantics for an experimental concurrent language inspired by the spiking neural P systems. At syntactic level, the language provides constructions for specifying the neurons, synapses and rules with time delays defining a spiking neural P system. The denotational semantics presented in this paper is designed by using continuations. We employ metric spaces, including a metric powerdomain to describe the nondeterministic behaviour. Our denotational semantics describes accurately the time delays between firings and spikings, the nondeterministic behaviour and the synchronized functioning that are specific of a spiking neural P system. An implementation in the functional language Haskell is also provided; it can be tested and evaluated, being available for software experiments.

By using the mathematical methodology of metric semantics and continuation semantics for concurrency (CSC) we design semantic models for a concurrent language extended with multiparty synchronization based on Hoare's CSP. We present a new kind of domain for CSC, where the structure of continuations is expressed by using functions which map computations to computations. We study the abstractness of CSC, by using a new optimality criterion specific to continuation semantics, that we call k weak abstractness - a weaker version of Milner's full abstractness criterion.

In recent work we have introduced an experimental concurrent programming language which supports a systematic approach to performance analysis and formal verification correlated with a programming style called performance evaluation programming [19]. For the purpose of formal verification, the ranges of variables must be bounded and concurrent programs are translated into corresponding (finite state) Continuous Time Markov Chains (CTMCs) which are analyzed by using the PRISM tool. Activities in a CTMC model are abstracted by their rates. In the language introduced in [19] an activity is the evaluation of a function expressed in a functional sub-language. The solution presented in [19] supports formal verification in a systematic manner, but not automatically, requiring the programmer to generate certain data for the performance evaluation experiments. In this paper we refine the design of the functional sub-language introduced in [19] by using concepts of functional programming with dependent types. We use dependent types to control the ranges of variables. The solution presented in this paper is devised to support automatic performance evaluation and formal verification of (bounded versions of) concurrent programs.

We present a denotational semantics for a simple concurrent language based on Milner's CCS extended with multiparty synchronous interactions. We show that our denotational model is weakly abstract with respect to a corresponding operational semantics. The denotational semantics is designed with metric spaces and continuation semantics for concurrency. The significance of the results presented in this paper is given also by the flexibility provided by the continuations technique.

CARMA (Collective Adaptive Resource-Sharing Markovian Agents) is a recently developed stochastic process algebra language which provides constructions for specifying the behavior of collective adaptive systems. By using CARMA and membrane computing patterns, in this paper we develop and analyze a model of the immune system response against virus attacks. By varying the rates of virus propagation, replication and destruction in our CARMA model, we investigate formal conditions for successful immune responses.

We present a denotational semantics designed with continuations for a concurrent language providing a mechanism for synchronous communication, together with constructions for process creation, remote process destruction and cloning. We accomplish the semantic investigation in the mathematical framework of complete metric spaces.

We investigate the abstractness of denotational models designed with continuation semantics for concurrency over metric spaces. Although there exist papers using continuations in the denotational semantics of concurrent languages, we are not aware of any full abstractness result for a concurrent language designed with continuations. Therefore we introduce a new criterion that we name weak abstractness; it preserves the correctness condition, but relaxes the completeness condition of the full abstractness criterion. Weak abstractness may be useful for a wide class of denotational models designed with continuations in which full abstractness is difficult (or impossible) to achieve. To illustrate this approach we present a denotational semantics for a simple asynchronous concurrent language designed with continuation semantics over metric spaces. We show that this denotational semantics is weakly abstract with respect to a corresponding operational model.

We present a denotational semantics designed in continuation-passing style (CPS) for an abstract language providing operators for nondeterministic choice, sequential and parallel composition, and a general mechanism of interaction between multisets of distributed actions. We show that the basic law s of concurrent systems are satisfied in this semantics. Next, by customizing the behavior of continuations we obtain denotational semantics for a couple of concurrent languages and a nature-inspired formalism. The languages discussed include Hoare’s communicating sequential processes (CSP), and two formalisms based on multiparty interactions: a version of CSP extended with communication and synchronization on multiple channels, and a language similar to a process algebra for DNA computing introduced by Cardelli. We accomplish the semantic investigation in the mathematical framework of complete metric spaces.

In this paper we present a mathematical model for a class of membrane systems, emphasizing on constructions of the denotational semantics as fixed points over complete metric spaces (to describe the semantics of multiset rewriting) and metric powerdomains (to describe the nondeterministic behaviour). We use the continuation-passing style, a technique providing enough flexibility for handling the concept of maximal parallelism and for describing the specific interactions in a membrane system. An important feature of the denotational approach is that it provides a compositional view of the membrane systems. Moreover, the semantics can be implemented naturally in a functional programming language; the implementation in Haskell is provided, and it is freely available for software experiments.