Search

In this work, we discuss the realisability problem for ranking-based semantics in the area of abstract argumentation. So, for a given ranking and ranking-based semantics, we want to find an AF s.t. the selected ranking-based semantics induces our ranking when applied to the AF. We show that this question can be answered trivially with yes for a number of ranking-based semantics, i.e. for every ranking we can find such an AF. In addition to the discussion about the realisability problem, we also introduce a new equivalence notion for argumentation frameworks. We call two AFs ranking equivalent if they have the same ranking for a ranking-based semantics.

There have been investigations into type-theoretic foundations for metaprogramming, notably Davies and Pfenning���s (2001) treatment in S4 modal logic, where code evaluating to values of type A is given the modal type Code A (���A in the original paper). Recently Kavvos (2017) extended PCF with Code A and intensional recursion, understood as the deductive form of the GL (G��del-L��b) axiom in provability logic, but the resulting type system is logically inconsistent. Inspired by staged computation, we observe that a term of type Code A is, in general, code to be evaluated in a next stage, whereas S4 modal type theory is a special case where code can be evaluated in the current stage, and the two types of code should be discriminated. Consequently, we use two separate modalities ��� and ��� to model S4 and GL respectively in a unified categorical framework while retaining logical consistency. Following Kavvos��� (2017) novel approach to the semantics of intensionality, we interpret the two modalities in the P-category of assemblies and trackable maps. For the GL modality ��� in particular, we use guarded type theory to articulate what it means by a ���next��� stage and to model intensional recursion by guarded recursion together with Kleene���s second recursion theorem. Besides validating the S4 and GL axioms, our model better captures the essence of intensionality by refuting congruence (so that two extensionally equal terms may not be intensionally equal) and internal quoting (both A ��� ���A and A ��� ���A). Our results are developed in (guarded) homotopy type theory and formalised in Agda., LIPIcs, Vol. 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), pages 14:1-14:17

This paper describes two results within the context of Petri net synthesis from labelled transition systems. We consider a set of structural properties of transition systems, and we show that, given such properties, it is possible to re-engineer a Petri net realisation into one which lies inside the set of marked graphs, a well-understood and useful class of Petri nets. The first result originates from Petri net based workflow specifications, where it is desirable that k customers can share a system without mutual interferences. In a Petri net representation of a workflow, the presence of k customers can be modelled by an initial k-marking, in which the number of tokens on each place is a multiple of k. For any initial k-marking with k ≥ 2 , we show that other desirable assumptions such as reversibility and persistence suffice to guarantee marked graph realisability. For the case that k = 1 , we show that the existence of certain cycles, along with other properties such as reversibility and persistence, again suffices to guarantee marked graph realisability.

International audience; This paper proposes a correct-by-construction method to build realizable choreographies described using conversation protocols (CPs). We define a new language consisting of an operators set for incremental construction of CPs. We suggest an asynchronous model described with the Event-B method and its refinement strategy, ensuring the scalability of our approach.

16 pages; International audience; This paper concerns the second order marginals of biphased random media. We give discriminating necessary conditions for a bivariate function to be such a valid marginal, and illustrate our study with two practical applications: (1) the spherical variograms are valid indicator variograms if and only if they are multiplied by a sufficiently small constant, which upper bound is estimated, and (2) not every covariance/indicator variogram can be obtained with a Gaussian level set. The theoretical results backing this study are contained in a companion paper.

Distributed software systems change dynamically due to the evolution of their environment and/or requirements, their internal designing policies, and/or their specification bugs which must be fixed. Hence, checking system changes must be run continuously. Such systems are usually composed of distributed software entities (called peers) interacting with each other through message exchanges, and this is to fulfil a common goal. The goal is often specified by a conversation protocol (CP), i.e. sequences of sent messages. If there exists a set of peers implementing CP, then CP is said to be realisable. In this paper, we propose a stepwise approach for checking whether an evolution, i.e. adding and/or removing messages and/or peers, can be applied to a CP that was realisable before updating it.We define a set of correct evolution patterns and we suggest an algebra of CP evolution. Our approach ensures that CP evolution preserves the realisability condition.

International audience; Distributed software systems are often built by composing independent and autonomous peers with cross-organisational interaction and no centralised control. These peers can be administrated and executed by geographically distributed and autonomous companies. In a top-down design of distributed software systems, the peers' interaction is often described by a global specification called Conversation Protocol (CP) and one have to check its realisability i.e., whether there exists a set of peers implementing this CP. In dynamic environments, CP needs to be updated wrt. new environment changes and end-user interaction requirements. This paper tackles CP evolution such that its realisability must be preserved. We define some evolution patterns and prove that they ensure the realisability. We also show how our proposal can be supported by existing methods and tools based on refinement and theorem proving, using the event-B langage and RODIN development tools.

We provide a characterization of the realisable set covariograms, bringing a rigorous yet abstract solution to the $S\_2$ problem in materials science. Our method is based on the covariogram functional for random mesurable sets (RAMS) and on a result about the representation of positive operators in a locally compact space. RAMS are an alternative to the classical random closed sets in stochastic geometry and geostatistics, they provide a weaker framework allowing to manipulate more irregular functionals, such as the perimeter. We therefore use the illustration provided by the $S\_{2}$ problem to advocate the use of RAMS for solving theoretical problems of geometric nature. Along the way, we extend the theory of random measurable sets, and in particular the local approximation of the perimeter by local covariograms., 35pp

We study existence of random elements with partially specified distributions. The technique relies on the existence of a positive extension for linear functionals accompanied by additional conditions that ensure the regularity of the extension needed for interpreting it as a probability measure. It is shown in which case the extension can be chosen to possess some invariance properties. The results are applied to the existence of point processes with given correlation measure and random closed sets with given two-point covering function or contact distribution function. It is shown that the regularity condition can be efficiently checked in many cases in order to ensure that the obtained point processes are indeed locally finite and random sets have closed realisations., Comment: Published in at http://dx.doi.org/10.1214/13-AAP990 the Annals of Applied Probability (http://www.imstat.org/aap/) by the Institute of Mathematical Statistics (http://www.imstat.org)

– The present paper aims at analysing the deep pragmatic equilavence relation existing between the so called Spanish support verb constructions formed by a verb + noun (hacer+sugerencia; dar+permiso). We will focus our attention on the functioning of such expressions as speech acts in order to demonstrate that on the basis of their semantic characteristics, there no always exists a parfect equivalence between the verbal expression and the verb as such in terms of realizing a speech act.

This dissertation explores the roles of polarities and focussing in various aspects of Computational Logic. These concepts play a key role in the the interpretation of proofs as programs, a.k.a. the Curry-Howard correspondence, in the context of classical logic. Arising from linear logic, they allow the construction of meaningful semantics for cut-elimination in classical logic, some of which relate to the Call-by-Name and Call-by-Value disciplines of functional programming. The first part of this dissertation provides an introduction to these interpretations, highlighting the roles of polarities and focussing. For instance: proofs of positive formulae provide structured data, while proofs of negative formulae consume such data; focussing allows the description of the interaction between the two kinds of proofs as pure pattern-matching. This idea is pushed further in the second part of this dissertation, and connected to realisability semantics, where the structured data is interpreted algebraically, and the consumption of such data is modelled with the use of an orthogonality relation. Most of this part has been proved in the Coq proof assistant. Polarities and focussing were also introduced with applications to logic programming in mind, where computation is proof-search. In the third part of this dissertation, we push this idea further by exploring the roles that these concepts can play in other applications of proof-search, such as theorem proving and more particularly automated reasoning. We use these concepts to describe the main algorithm of SAT-solvers and SMT-solvers: DPLL. We then describe the implementation of a proof-search engine called Psyche. Its architecture, based on the concept of focussing, offers a platform where smart techniques from automated reasoning (or a user interface) can safely and trustworthily be implemented via the use of an API., Dissertation submitted towards the degree of Habilitation \`a Diriger des Recherches. Universit\'e Paris-Sud. 212 pages. Thesis publicly defended on 17th December 2014 before a panel consisting of Laurent Regnier, Wolfgang Ahrendt, Hugo Herbelin, Frank Pfenning, Sylvain Conchon, David Delahaye, Didier Galmiche, Christine Paulin-Mohring

Mental representations, Swiatczak (Minds Mach 21:19-32, 2011) argues, are fundamentally biochemical and their operations depend on consciousness; hence the computational theory of mind, based as it is on multiple realisability and purely syntactic operations, must be wrong. Swiatczak, however, is mistaken. Computation, properly understood, can afford descriptions/explanations of any physical process, and since Swiatczak accepts that consciousness has a physical basis, his argument against computationalism must fail. Of course, we may not have much idea how consciousness (itself a rather unclear plurality of notions) might be implemented, but we do have a hypothesis-that all of our mental life, including consciousness, is the result of computational processes and so not tied to a biochemical substrate. Like it or not, the computational theory of mind remains the only game in town. © Springer Science+Business Media B.V. 2011.

Seeking a general framework for reasoning about and comparing programming languages, we derive a new view of Milner's CCS. We construct a category E of 'plays', and a subcategory V of 'views'. We argue that presheaves on V adequately represent 'innocent' strategies, in the sense of game semantics. We equip innocent strategies with a simple notion of interaction. We then prove decomposition results for innocent strategies, and, restricting to presheaves of finite ordinals, prove that innocent strategies are a final coalgebra for a polynomial functor derived from the game. This leads to a translation of CCS with recursive equations. Finally, we propose a notion of 'interactive equivalence' for innocent strategies, which is close in spirit to Beffara's interpretation of testing equivalences in concurrency theory. In this framework, we consider analogues of fair testing and must testing. We show that must testing is strictly finer in our model than in CCS, since it avoids what we call 'spatial unfairness'. Still, it differs from fair testing, and we show that it coincides with a relaxed form of fair testing., Comment: 53 pages. Expanded version of ICE '11 paper DOI 10.4204/EPTCS.59.2

This paper revisits models of typed lambda-calculus based on filters of intersection types: By using non-idempotent intersections, we simplify a methodology that produces modular proofs of strong normalisation based on filter models. Non-idempotent intersections provide a decreasing measure proving a key termination property, simpler than the reducibility techniques used with idempotent intersections. Such filter models are shown to be captured by orthogonality techniques: we formalise an abstract notion of orthogonality model inspired by classical realisability, and express a filter model as one of its instances, along with two term-models (one of which captures a now common technique for strong normalisation). Applying the above range of model constructions to Curry-style System F describes at different levels of detail how the infinite polymorphism of System F can systematically be reduced to the finite polymorphism of intersection types.

Submitted by Delfim F. M. Torres (delfim@ua.pt) on 2011-09-26T19:41:21Z No. of bitstreams: 1 [177]BackwardLinearControlSystemsTimeScales.pdf: 188496 bytes, checksum: ce10805b6eacf0b24d3e1c888635fce4 (MD5) Made available in DSpace on 2011-10-11T11:58:21Z (GMT). No. of bitstreams: 1 [177]BackwardLinearControlSystemsTimeScales.pdf: 188496 bytes, checksum: ce10805b6eacf0b24d3e1c888635fce4 (MD5) Previous issue date: 2010 CEOC CIDMA FCT FEDER/POCI 2010

In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni–Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. In this paper we develop a semantics of SLR using BCK -algebras consisting of certain polynomial-time algorithms. It will follow from this semantics that safe recursion with arbitrary result type built up from N and ⊸ as well as recursion over trees and other data structures remains within polynomial time. In its original formulation SLR supported only natural numbers and recursion on notation with first-order functional result type.

Pomsets are a model of concurrent computations introduced by Pratt. We adopt pomsets as a syntax-oblivious specification model of distributed systems where coordination happens via asynchronous message-passing. In this paper, we study conditions that ensure a specification expressed as a set of pomsets can be faithfully realised via communicating automata. Our main contributions are (i) the definition of a realisability condition accounting for termination soundness, (ii) conditions accounting for ‘‘multi-threaded’’ participants, and (iii) an algorithm to check our realisability conditions directly over pomsets, (iv) an analysis of the algorithm and its benchmarking attained with a prototype implementation.

This thesis introduces an extension of the Calculus of Constructions of Coquand and Huet which allows the extraction of certified programs from constructive proofs. A modified realisability notion is introduced and its properties are studied. An impredicative encoding of a large class of inductive definitions is proposed., Cette thèse propose une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité modifiée est introduite et étudiée. Un codage imprédicatif d'une large classe de définitions inductives est proposé.

5th International Conference on Model-Driven Engineering and Software Development (MODELSWARD) -- FEB 19-21, 2017 -- Porto, PORTUGAL Ozkaya, Mert/0000-0003-2329-9925; Ozkaya, Mert/0000-0002-3464-6489 WOS:000413238000036 With the advent of software architectures, architectural languages have become an active research area for the specification of software architectures in terms of components & connectors and for some extra capabilities such as formal analysis and code generation. In this paper, the existing architectural languages have been analysed for two important language features - i.e., interaction protocols and realisability. The analysis results show that only a few languages support interaction protocols via their first-class connector elements (also referred to as complex connectors). However, complex connectors of those languages lead to unrealisable specifications due to enabling global constraints which may not be possible for distributed systems. Therefore, practitioners cannot implement the system in the way specified, and any analyses (e.g., performance) made on the unrealisable specifications will all be invalid. project of the Scientific and Technological Research Council of Turkey (TUBITAK)Turkiye Bilimsel ve Teknolojik Arastirma Kurumu (TUBITAK) [215E159] This work has been supported by the project of the Scientific and Technological Research Council of Turkey (TUBITAK), Grant No: 215E159.