Person:
Frutos Escrig, David De

First Name

David De

Last Name

Frutos Escrig

URI

https://hdl.handle.net/20.500.14352/75661

Affiliation

Universidad Complutense de Madrid

Faculty / Institute

Ciencias Matemáticas

Department

Sistemas Informáticos y Computación

Area

Lenguajes y Sistemas Informáticos

Identifiers

Full item page

Search Results

Now showing 1 - 10 of 62

Simulations up-to and canonical preorders
(Electronic Notes in Theoretical Computer Science, 2007) Frutos Escrig, David De; Gregorio Rodríguez, Carlos
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 all semantic preorders coarser than the ready simulation preorder in the linear time-branching time spectrum. An interesting but unexpected result is that, when built from an equivalence relation, the simulation up-to is a canonical preorder whose kernel is the given equivalence relation. These canonical preorders have several nice properties, the main being that since all of them are defined in a homogeneous way, their properties can be proved in a generic way. In particular, we present an axiomatic characterization of each of these canonical preorders, that is obtained just by adding a single axiom to the axiomatization of the original equivalence relation. This gives us an alternative axiomatization for every axiomatizable preorder in the linear time-branching time spectrum, whose correctness and completeness can be proved once and for all.
Bisimulations Up-to for the Linear Time Branching Time Spectrum
(CONCUR 2005 – Concurrency Theory : 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings, 2005) Frutos Escrig, David De; Gregorio Rodríguez, Carlos; Abadi, Martín; de Alfaro, Luca
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 variant of the bisimulation up-to technique in which we allow the use of a given preorder relation. We prove that under some technical conditions our bisimulations up-to characterise the kernel of the given preorder. It is remarkable that the adequate orientation of the ordering relation is crucial to get this result. As a corollary, we get nice coinductive characterisations of all the axiomatic semantic equivalences in Van Glabbeek’s spectrum. Although we first prove our results for finite processes, reasoning by induction, then we see, by using continuity arguments, that they are also valid for infinite (finitary) processes.
Preserving contexts for soft conformance relation
(Formal Approaches to Software Testing : 4th International Workshop, FATES 2004, Linz, Austria, September 21, 2004, Revised Selected Papers, 2005) Frutos Escrig, David De; Gregorio Rodríguez, Carlos; Grabowski, Jens; Nielsen, Brian
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, we concentrate on the study of the conditions under which a context preserves the soft conformance relation of two agents. These conditions depend both on the specification and the implementation in the conformance relation and also on the context. Since the addition of extraneous actions to the implementation allows to define malicious contexts that would not preserve the conformance relation, such a characterisation of the family of contexts preserving each individual pair (implementation and specification) in the conformance relation is the best result that can be expected in this direction.
Constrained simulations, nested simulation semantics and counting bisimulations
(Proceedings of the Seventh Spanish Conference on Programming and Computer Languages (PROLE 2007), 2008) Frutos Escrig, David De; Gregorio Rodríguez, Carlos
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 formal meaning and the properties of concurrent processes. In this paper we present the notion of constrained simulation that, although rather simple, allows us to find general results for a wide family of semantics. In particular, we provide an axiomatization for both the preorder and the equivalence induced by any constrained simulation. Nested simulations are constrained simulations and therefore our results can be instantiated directly to them. Besides, constrained simulations suggest the definition of a new family of semantics, generalised nested simulation semantics, constructed over the base of any order relation, instead of plain simulation. Finally, we conclude the study of the (generalised) nested semantics defining a generalisation of bisimulation relations, counting bisimulation, that allows us to define a characterisation of nested semantics in terms of a bisimulation-like game.
On the unification of process semantics: observational semantics
(SOFSEM 2009: Theory and Practice of Computer Science : 35th Conference on Current Trends in Theory and Practice of Computer Science, Špindlerův Mlýn, Czech Republic, January 24-30, 2009. Proceedings, 2009) Frutos Escrig, David De; Gregorio Rodríguez, Carlos; Palomino Tarjuelo, Miguel; Nielsen, Mogens; Kucera, Antonin; Miltersen, Peter Bro; Palamidessi, Castuscia; Tuma, Petr; Valencia, Frank
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 available. We have discovered how to unify them, both in an observational framework and in an equational framework. In this first part of our study we present the observational semantics, that stresses the differences between the simulation (branching) semantics and the extentional (linear) semantics. As a result we rediscover the classification in van Glabbeek’s spectrum and shed light on it, obtaining a framework where we can consider all the semantics in the spectrum at the same time. Also, we have discovered some “lost links” that correspond to semantics, possibly not too interesting (at the moment), that provide a clearer picture of the spectrum.
Axiomatizing weak simulation semantics over BCCSP
(Theoretical computer science, 2014) Aceto, Luca; Frutos Escrig, David De; Gregorio Rodríguez, Carlos
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 behaviours. In particular, the article focuses on the (pre)congruences associated with the weak simulation, the weak complete simulation and the weak ready simulation preorders. We present results on the (non)existence of finite (ground-)complete (in)equational axiomatizations for each of these behavioural semantics. The axiomatization of those semantics using conditional equations is also discussed in some detail.
Multiset Bisimulations as a Common Framework for Ordinary and Probabilistic Bisimulations
(Formal Techniques for Networked and Distributed Systems – FORTE 2008 : 28th IFIP WG 6.1 International Conference Tokyo, Japan, June 10-13, 2008 Proceedings, 2008) Frutos Escrig, David De; Palomino Tarjuelo, Miguel; Fábregas Alfaro, Ignacio; Suzuki, Kenji; Higashino, Teruo; Yasumoto, Keiichi; El-Fakih, Khaled
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 distributions functors with the multiset functor by means of adequate natural transformations. This leads us to the general topic that we investigate in the paper: a natural transformation from a functor F to another G transforms F-bisimulations into G-bisimulations but, in general, it is not possible to express G-bisimulations in terms of F-bisimulations. However, they can be characterized by considering Hughes and Jacobs’ notion of simulation, taking as the order on the functor F the equivalence induced by the epi-mono decomposition of the natural transformation relating F and G. We also consider the case of alternating probabilistic systems where non-deterministic and probabilistic choices are mixed, although only in a partial way, and extend all these results to categorical simulations.
Decidability problems in Petri nets with names and replication
(Fundamenta informaticae, 2010) Rosa Velardo, Fernando; Frutos Escrig, David De
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 undecidable) and ν-RN systems (RN extended with name creation, which are Turing-complete, so that coverability is undecidable), in order to obtain decidability of reachability and coverability, respectively. We prove that if we forbid synchronizations between the different components in a RN system, then reachability is still decidable. Similarly, if we forbid name communication between the different components in a ν-RN system, or restrict communication so that it is allowed only for a given finite set of names, we obtain decidability of coverability. Finally, we consider a polyadic version of ν-PN (P/T nets extended with name creation), that we call pν-PN, in which tokens are tuples of names. We prove that pν-PN are Turing complete, and discuss how the results obtained for ν-RN systems can be translated to them.
Special issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015)
(Acta Informatica, 2017) Aceto, L.; Frutos Escrig, David De
Investigating reversibility of steps in Petri nets
(Fundamenta informaticae, 2021) Frutos Escrig, David De; Koutny, Maciej; Mikulski, Łukasz
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 reversing the effect of the execution of groups of actions (steps). Using Petri nets as a system model, we introduce concepts related to this new scenario, generalising notions used in the single action case. We then present properties arising when reverse actions are allowed in place/transition nets (PT-nets). We obtain both positive and negative results, showing that allowing steps makes reversibility more problematic than in the interleaving/sequential case. In particular, we demonstrate that there is a crucial difference between reversing steps which are sets and those which are true multisets. Moreover, in contrast to sequential semantics, splitting reverses does not lead to a general method for reversing bounded PT-nets. We then show that a suitable solution can be obtained by combining split reverses with weighted read arcs.