8 Search Results for "Winskel, Glynn"

Document
DOI: 10.4230/LIPIcs.CALCO.2019.9
Causal Unfoldings

Authors: Marc de Visme and Glynn Winskel

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
In the simplest form of event structure, a prime event structure, an event is associated with a unique causal history, its prime cause. However, it is quite common for an event to have disjunctive causes in that it can be enabled by any one of multiple sets of causes. Sometimes the sets of causes may be mutually exclusive, inconsistent one with another, and sometimes not, in which case they coexist consistently and constitute parallel causes of the event. The established model of general event structures can model parallel causes. On occasion however such a model abstracts too far away from the precise causal histories of events to be directly useful. For example, sometimes one needs to associate probabilities with different, possibly coexisting, causal histories of a common event. Ideally, the causal histories of a general event structure would correspond to the configurations of its causal unfolding to a prime event structure; and the causal unfolding would arise as a right adjoint to the embedding of prime in general event structures. But there is no such adjunction. However, a slight extension of prime event structures remedies this defect and provides a causal unfolding as a universal construction. Prime event structures are extended with an equivalence relation in order to dissociate the two roles, that of an event and its enabling; in effect, prime causes are labelled by a disjunctive event, an equivalence class of its prime causes. With this enrichment a suitable causal unfolding appears as a pseudo right adjoint. The adjunction relies critically on the central and subtle notion of extremal causal realisation as an embodiment of causal history.
Cite as

Marc de Visme and Glynn Winskel. Causal Unfoldings. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{devisme_et_al:LIPIcs.CALCO.2019.9,
  author =	{de Visme, Marc and Winskel, Glynn},
  title =	{{Causal Unfoldings}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.9},
  URN =		{urn:nbn:de:0030-drops-114376},
  doi =		{10.4230/LIPIcs.CALCO.2019.9},
  annote =	{Keywords: Event Structures, Parallel Causes, Causal Unfolding, Probability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.5
The True Concurrency of Herbrand's Theorem

Authors: Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. In the general case, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers. In this paper, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems, thereby exposing the concurrency underlying the computational content of classical proofs. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers implicit in proofs. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model.
Cite as

Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel. The True Concurrency of Herbrand's Theorem. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{alcolei_et_al:LIPIcs.CSL.2018.5,
  author =	{Alcolei, Aurore and Clairambault, Pierre and Hyland, Martin and Winskel, Glynn},
  title =	{{The True Concurrency of Herbrand's Theorem}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.5},
  URN =		{urn:nbn:de:0030-drops-96723},
  doi =		{10.4230/LIPIcs.CSL.2018.5},
  annote =	{Keywords: Herbrand's theorem, Game semantics, True concurrency}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.81
Distributed Strategies Made Easy

Authors: Simon Castellan, Pierre Clairambault, and Glynn Winskel

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Distributed/concurrent strategies have been introduced as special maps of event structures. As such they factor through their "rigid images," themselves strategies. By concentrating on such "rigid image" strategies we are able to give an elementary account of distributed strategies and their composition, resulting in a category of games and strategies. This is in contrast to the usual development where composition involves the pullback of event structures explicitly and results in a bicategory. It is shown how, in this simpler setting, to extend strategies to probabilistic strategies; and indicated how through probability we can track nondeterministic branching behaviour, that one might otherwise think lost irrevocably in restricting attention to "rigid image" strategies.
Cite as

Simon Castellan, Pierre Clairambault, and Glynn Winskel. Distributed Strategies Made Easy. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 81:1-81:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{castellan_et_al:LIPIcs.MFCS.2017.81,
  author =	{Castellan, Simon and Clairambault, Pierre and Winskel, Glynn},
  title =	{{Distributed Strategies Made Easy}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{81:1--81:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.81},
  URN =		{urn:nbn:de:0030-drops-81315},
  doi =		{10.4230/LIPIcs.MFCS.2017.81},
  annote =	{Keywords: Games, Strategies, Event Structures, Probability}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.12
Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or

Authors: Simon Castellan, Pierre Clairambault, and Glynn Winskel

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
Although Plotkin’s parallel-or is inherently deterministic, it has a non-deterministic interpretation in games based on (prime) event structures - in which an event has a unique causal history - because they do not directly support disjunctive causality. General event structures can express disjunctive causality and have a more permissive notion of determinism, but do not support hiding. We show that (structures equivalent to) deterministic general event structures do support hiding, and construct a new category of games based on them with a deterministic interpretation of aPCFpor, an affine variant of PCF extended with parallel-or. We then exploit this deterministic interpretation to give a relaxed notion of determinism (observable determinism) on the plain event structures model. Putting this together with our previously introduced concurrent notions of well-bracketing and innocence, we obtain an intensionally fully abstract model of aPCFpor.
Cite as

Simon Castellan, Pierre Clairambault, and Glynn Winskel. Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{castellan_et_al:LIPIcs.FSCD.2017.12,
  author =	{Castellan, Simon and Clairambault, Pierre and Winskel, Glynn},
  title =	{{Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.12},
  URN =		{urn:nbn:de:0030-drops-77219},
  doi =		{10.4230/LIPIcs.FSCD.2017.12},
  annote =	{Keywords: Game semantics, parallel-or, concurrent games, event structures, full abstraction}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.41
Strategies with Parallel Causes

Authors: Marc de Visme and Glynn Winskel

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We imagine a team Player engaging a team Opponent in a distributed game. Such games and their strategies have been formalised within event structures. However there are limitations in founding strategies on traditional event structures. Sometimes a probabilistic distributed strategy relies on benign races where, intuitively, several members of team Player may race each other to make a common move. Although there exist event structures which support such parallel causes, in which an event is enabled in several compatible ways, they do not support an operation of hiding central to the composition of strategies; nor do they support probability adequately. An extension of traditional event structures is devised which supports parallel causes and hiding, as well as the mix of probability and nondeterminism needed to account for probabilistic distributed strategies. The extension is located within existing models for concurrency and tested in the construction of a bicategory of probabilistic distributed strategies with parallel causes.
Cite as

Marc de Visme and Glynn Winskel. Strategies with Parallel Causes. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 41:1-41:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{devisme_et_al:LIPIcs.CSL.2017.41,
  author =	{de Visme, Marc and Winskel, Glynn},
  title =	{{Strategies with Parallel Causes}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{41:1--41:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.41},
  URN =		{urn:nbn:de:0030-drops-76800},
  doi =		{10.4230/LIPIcs.CSL.2017.41},
  annote =	{Keywords: Games, Strategies, Event Structures, Parallel Causes, Probability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.276
Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models

Authors: Vincent Danos, Jerome Feret, Walter Fontana, Russell Harmer, Jonathan Hayman, Jean Krivine, Chris Thompson-Walsh, and Glynn Winskel

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
In this paper, we introduce a novel way of constructing concise causal histories (pathways) to represent how specified structures are formed during simulation of systems represented by rule-based models. This is founded on a new, clean, graph-based semantics introduced in the first part of this paper for Kappa, a rule-based modelling language that has emerged as a natural description of protein-protein interactions in molecular biology [Bachman 2011]. The semantics is capable of capturing the whole of Kappa, including subtle side-effects on deletion of structure, and its structured presentation provides the basis for the translation of techniques to other models. In particular, we give a notion of trajectory compression, which restricts a trace culminating in the production of a given structure to the actions necessary for the structure to occur. This is central to the reconstruction of biochemical pathways due to the failure of traditional techniques to provide adequately concise causal histories, and we expect it to be applicable in a range of other modelling situations.
Cite as

Vincent Danos, Jerome Feret, Walter Fontana, Russell Harmer, Jonathan Hayman, Jean Krivine, Chris Thompson-Walsh, and Glynn Winskel. Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 276-288, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{danos_et_al:LIPIcs.FSTTCS.2012.276,
  author =	{Danos, Vincent and Feret, Jerome and Fontana, Walter and Harmer, Russell and Hayman, Jonathan and Krivine, Jean and Thompson-Walsh, Chris and Winskel, Glynn},
  title =	{{Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{276--288},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.276},
  URN =		{urn:nbn:de:0030-drops-38669},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.276},
  annote =	{Keywords: concurrency, rule-based models, graph rewriting, pathways, causality}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1755
The unfolding of general Petri nets

Authors: Jonathan Hayman and Glynn Winskel

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract
The unfolding of (1-)safe Petri nets to occurrence nets is well understood. There is a universal characterization of the unfolding of a safe net which is part and parcel of a coreflection from the category of occurrence nets to the category of safe nets. The unfolding of general Petri nets, nets with multiplicities on arcs whose markings are multisets of places, does not possess a directly analogous universal characterization, essentially because there is an implicit symmetry in the multiplicities of general nets, and that symmetry is not expressed in their traditional occurrence net unfoldings. In the present paper, we show how to recover a universal characterization by representing the symmetry in the behaviour of the occurrence net unfoldings of general Petri nets. We show that this is part of a coreflection between enriched categories of general Petri nets with symmetry and occurrence nets with symmetry.
Cite as

Jonathan Hayman and Glynn Winskel. The unfolding of general Petri nets. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 223-234, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{hayman_et_al:LIPIcs.FSTTCS.2008.1755,
  author =	{Hayman, Jonathan and Winskel, Glynn},
  title =	{{The unfolding of general Petri nets}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{223--234},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1755},
  URN =		{urn:nbn:de:0030-drops-17552},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1755},
  annote =	{Keywords: Petri nets, symmetry, unfolding}
}
Document
DOI: 10.4230/DagSemRep.144
Semantics of Concurrent Systems - Foundations and Applications (Dagstuhl Seminar 9619)

Authors: Manfred Droste, Ernst-Rüdiger Olderog, Bernhard Steffen, and Glynn Winskel

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Manfred Droste, Ernst-Rüdiger Olderog, Bernhard Steffen, and Glynn Winskel. Semantics of Concurrent Systems - Foundations and Applications (Dagstuhl Seminar 9619). Dagstuhl Seminar Report 144, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1996)

Copy BibTex To Clipboard

@TechReport{droste_et_al:DagSemRep.144,
  author =	{Droste, Manfred and Olderog, Ernst-R\"{u}diger and Steffen, Bernhard and Winskel, Glynn},
  title =	{{Semantics of Concurrent Systems - Foundations and Applications (Dagstuhl Seminar 9619)}},
  pages =	{1--18},
  ISSN =	{1619-0203},
  year =	{1996},
  type = 	{Dagstuhl Seminar Report},
  number =	{144},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.144},
  URN =		{urn:nbn:de:0030-drops-150310},
  doi =		{10.4230/DagSemRep.144},
}
  • Refine by Author
  • 8 Winskel, Glynn
  • 3 Clairambault, Pierre
  • 2 Castellan, Simon
  • 2 Hayman, Jonathan
  • 2 de Visme, Marc
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 Event Structures
  • 3 Probability
  • 2 Game semantics
  • 2 Games
  • 2 Parallel Causes
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 3 2017
  • 1 1996
  • 1 2008
  • 1 2012
  • 1 2018
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact