Información del autor
Autor Frutos Escrig, David de |
Documentos disponibles escritos por este autor (58)
![](./images/expand_all.gif)
![](./images/collapse_all.gif)
![Selecciones disponibles](./images/orderby_az.gif)
![]()
texto impreso
Pure names are identifiers with no relation between them, except equality and inequality. In previous works we have extended P/T nets with the capability of creating and managing pure names, obtaining ?-PNs and proved that they are strictly well[...]![]()
texto impreso
Con ocasión del centenario del nacimiento de Alan Turing, y la celebración a nivel internacional de «The Alan Turing Year», con el que se conmemora el mismo a nivel internacional, presentamos una visión personal de su obra, exponiendo de manera [...]![]()
texto impreso
We present a new testing semantics, called friendly testing, whose main property is that the induced preorder between processes ?fr is consistent with the conformance relation, and so we have, for instance,a ?b ?fr a ?fr a +b. The new theory is [...]![]()
texto impreso
Aceto, Luca ; Frutos Escrig, David de ; Gregorio Rodríguez, Carlos ; Ingolfsdottir, Anna | Springer | 2011Ready simulation has proven to be one of the most significant semantics in process theory. It is at the heart of a number of general results that pave the way to a comprehensive understanding of the spectrum of process semantics. Since its origi[...]![]()
texto impreso
This paper is devoted to the study of the (in)equational theory of the largest (pre)congruences over the language BCCSP induced by variations on the classic simulation preorder and equivalence that abstract from internal steps in process behavio[...]![]()
texto impreso
Barozzini, David ; Frutos Escrig, David de ; Della Monica, Dario ; Montanari, Angelo ; Sala, Pietro | Elsevier | 2020-04-12In the last years, some extensions of ?-regular languages, namely, ?B-regular (?-regular languages extended with boundedness), ?S-regular (?-regular languages extended with strong unboundedness), and ?BS-regular languages (the combination of ?B-[...]![]()
texto impreso
We define (bi)simulations up-to a preorder and show how we can use them to provide a coinductive, (bi)simulation-like, characterisation of semantic (equivalences) preorders for processes. In particular, we can apply our results to all the semant[...]![]()
texto impreso
The definition of sos formats ensuring that bisimilarity on closed terms is a congruence has received much attention in the last two decades. For dealing with open terms, the congruence is usually lifted from closed terms by instantiating the fr[...]![]()
texto impreso
Coinductive definitions of semantics based on bisimulations have rather pleasant properties and are simple to use. In order to get coinductive characterisations of those semantic equivalences that are weaker than strong bisimulation we use a var[...]![]()
texto impreso
Branching bisimilarity and branching bisimilarity with explicit divergences are typically used in process algebras with silent steps when relating implementations to specifications. When an implementation fails to conform to its specification, i[...]![]()
texto impreso
n 1976, Plotkin introduced powerdomains adapting to them, in some sense, Egli- Milner's order. Lately, Smyth (1978) presented the same results starting from generating trees, and adding a new order that he denoted by 0. He also gave a characteri[...]![]()
texto impreso
There are two ways to define a semantics for process algebras: either directly by means of an equivalence relation or by means of a preorder whose kernel is the desired equivalence. We are interested in the relationship between these two present[...]![]()
texto impreso
Bisimulation captures in a coinductive way the quivalence between processes, or trees. Several authors have defined bisimulation distances based on the bisimulation game. However, this approach becomes too local: whenever we have in one of the c[...]![]()
texto impreso
This note shows that the complete and the ready simulation preorders do not have a finite inequational basis over the language BCCSP when the set of actions is a singleton. Moreover, the equivalences induced by those preorders do not have a fini[...]![]()
texto impreso
Nested simulations define an interesting hierarchy of semantic preorders and equivalences in which every semantics refines the previous one and it is refined by the following. This nested nature provides a fruitful framework for the study of the[...]![]()
texto impreso
We prove several decidability and undecidability results for ?-PN, an extension of P/T nets with pure name creation and name management. We give a simple proof of undecidability of reachability, by reducing reachability in nets with inhibitor ar[...]![]()
texto impreso
Timed-arc Petri nets (TAPN’s) are not Turing powerful, because, in particular, they cannot simulate a counter with zero testing. Thus, we could think that this model does not increase significantly the expressiveness of untimed Petri nets. But t[...]![]()
texto impreso
In this paper we study decidability of several extensions of P/T nets with name creation and/or replication. In particular, we study how to restrict the models of RN systems (P/T nets extended with replication, for which reachability is undecida[...]![]()
texto impreso
In previous works we defined ?-APNs, an extension of P/T nets with the capability of creating and managing pure names. We proved that, though reachability is undecidable, coverability remains decidable for them. We also extended P/T nets with th[...]![]()
texto impreso
We prove several decidability and undecidability results for nu-PN, an extension of P/T nets with pure name creation and name management. We give a simple proof of undecidability of reachability, by reducing reachability in nets with inhibitor a[...]![]()
texto impreso
Recently several authors have proposed some notions of distance between processes that try to quantify “how far away” is a process to be related with some other with respect to a certain semantics. These proposals are usually based on the simula[...]![]()
texto impreso
In this paper we present a denotational semantics for a timed process algebra, which is fully abstract with respect to the must testing semantics previously developed [Lla96,LdFN96]. The domain of semantic processes is made up of consistent sets[...]![]()
texto impreso
Covariant-contravariant simulation and conformance simulation generalize plain simulation and try to capture the fact that it is not always the case that "the larger the number of behaviors, the better". We have previously studied their logical [...]![]()
texto impreso
PBC (Petri Box Calculus) is a process algebra where real parallelism of concurrent systems can be naturally expressed. One of its main features is the definition of a denotational semantics based on Petri nets, which emphasizes the structural as[...]![]()
texto impreso
Pure names are identifiers with no relation between them, except equality and inequality. In previous works we have extended P/T nets with the capability of creating and managing pure names, obtaining ?-APNs and proved that they are strictly wel[...]![]()
texto impreso
Aceto , Luca ; Fábregas, Ignacio ; Frutos Escrig, David de ; Ingolfsdottir, Anna ; Palomino, Miguel | EPTCS | 2011Covariant-contravariant simulation is a combination of standard (covariant) simulation, its contravariant counterpart and bisimulation. We have previously studied its logical characterization by means of the covariant-contravariant modal logic. [...]![]()
texto impreso
We present a new testing semantics, called friendly testing, whose main property is that the induced preorder between processes v fr is consistent with the conformance relation, and so we have, for instance, a \Phi b v fr a v fr a + b. The new t[...]![]()
texto impreso
Covariant-contravariant simulation and conformance simulation are two generalizations of the simple notion of simulation which aim at capturing the fact that it is not always the case that “the larger the number of behaviors, the better”. Theref[...]![]()
texto impreso
Our concrete objective is to present both ordinary bisimulations and probabilistic bisimulations in a common coalgebraic framework based on multiset bisimulations. For that we show how to relate the underlying powerset and probabilistic distribu[...]![]()
texto impreso
We study the relationship between name creation and replication in a setting of infinitestate communicating automata. By name creation we mean the capacity of dynamically producing pure names, with no relation between them other than equality or[...]![]()
texto impreso
We study the relationship between name creation and replication in a setting of infinite-state communicating automata. By name creation we mean the capacity of dynamically producing pure names, with no relation between them other than equality o[...]![]()
texto impreso
Bisimulation semantics are a very pleasant way to define the semantics of systems, mainly because the simplicity of their definitions and their nice coalgebraic properties. However, they also have some disadvantages: they are based on a sequenti[...]![]()
texto impreso
We present a study of the notion of coalgebraic simulation introduced by Hughes and Jacobs. Although in their original paper they allow any functorial order in their definition of coalgebraic simulation, for the simulation relations to have good[...]![]()
texto impreso
We study completeness of narrowing strategies for a class of programs defining (possibly partial and non-strict) functions by means of equations, with a lazy semantics, so that infinite values are also admissible. We consider a syntactical restr[...]![]()
texto impreso
In recent papers we have introduced Mobile Synchronizing Petri Nets, a new model for mobility based on coloured Petri Nets. It allows the description of systems composed of a collection of (possibly mobile) hardware devices and mobile agents, bo[...]![]()
texto impreso
Embedded-systems designers often use transition system-based notations for specifying, with respect to some refinement preorder, sets of deterministic implementations. This paper compares popular such refinement settings — ranging from transitio[...]![]()
texto impreso
The complexity of parallel systems has produced a large collection of semantics for processes, a classification of which is provided by Van Glabbeek's linear time-branching time spectrum; however, no suitable unified definitions were available. [...]![]()
texto impreso
We continue with the task of obtaining a unifying view of process semantics by considering in this case the logical characterization of the semantics. We start by considering the classic linear time-branching time spectrum developed by R.J. van [...]![]()
texto impreso
The complexity of parallel systems has produced a large collection of semantics for processes. Van Glabbeek’s linear time-branching time spectrum provides a classification of most of these semantics; however, no suitable unified definitions were[...]![]()
texto impreso
We present a model of probabilistic processes, which is an extension of CSP, on the basis of replacing internal non-determinism by generative probabilistic choices, and external non-determinism by reactive probabilistic choices. Our purpose when[...]![]()
texto impreso
This paper addresses the study of bisimulation based conformance relations in which input and output actions not presented in the specification are added to the implementation. A new definition, that we called soft conformance, is given. Then, w[...]![]()
texto impreso
We present probabilistic Ianov's schemes, studying their semantics and proving the equivalence between operational and denotational ones. We also study the equivalence of schemes relative to them; as usual all these equivalence problems are deci[...]![]()
texto impreso
Frutos Escrig, David de ; Gregorio Rodríguez, Carlos | Graz Univ. Technolgoy, Inst. Information Systems Computer Med. | 2006Bisimulation can be defined in a simple way using coinductive methods, and has rather pleasant properties. Ready similarity was proposed by Meyer et al. as a way to weakening the bisimulation equivalence thus getting a semantics defined in a sim[...]![]()
texto impreso
There have been quite a few proposals for behavioural equivalences for concurrent processes, and many of them are presented in Van Glabbeek’s linear time-branching time spectrum. Since their original definitions are based on rather different ide[...]![]()
texto impreso
Our objective is to extend the standard results of preservation and reflection of properties by bisimulations to the coalgebraic setting, as well as to study under what conditions these results hold for simulations. The notion of bisimulation is[...]![]()
texto impreso
Aceto, Luca ; Fábregas, Ignacio ; Frutos Escrig, David de ; Ingolfsdottir, Anna ; Palomino, Miguel | Springer | 2012This paper studies the relationships between three notions of behavioural preorder that have been proposed in the literature: refinement over modal transition systems, and the covariant-contravariant simulation and the partial bisimulation preor[...]![]()
texto impreso
Recently we have introduced Ambient Petri nets, as a multilevel extension of the Elementary Object Systems, that can be used to model the concept of nested ambients from the Ambient Calculus. Both mobile computing and mobile computation are supp[...]![]()
texto impreso
In reversible computations one is interested in the development of mechanisms allowing to undo the effects of executed actions. The past research has been concerned mainly with reversing single actions. In this paper, we consider the problem of [...]![]()
texto impreso
In this paper we define simulations up-to a preorder and show how we can use them to provide a coinductive, simulation-like, characterization of semantic preorders for processes. The result applies to a wide class of preorders, in particular to [...]![]()
texto impreso
We define and study some definitions of probabilistic powerdomains over domains in SFP. We give three definitions: the first one is based in the notion of probability distribution over a domain; the second in probabilistic generating trees, that[...]