Prehistoric Graph in Modal Derivations and Self-Referentiality

By terms-allowed-in-formulas capacity, Artemov’s Logic of Proofs LP Artemov includes self-referential formulas of the form t:?(t) that play a crucial role in the realization of modal logic S4 in LP, and in the Brouwer–Heyting–Kolmogorov semantics of intuitionistic logic via LP. In an earlier work appeared in the Proceedings of CSR 2010 the author defined prehistoric loop in a sequent calculus of S4, and verified its necessity to self-referentiality in S4?LP realization. In this extended version we generalize results there to T and K4, two modal logics smaller than S4 that yet call for self-referentiality in their realizations into corresponding justification logics JT and J4.     

ReSpecT Nets: Towards an Analysis Methodology for ReSpecT Specifications

A key feature for infrastructures providing coordination services is the ability to define the behaviour of coordination abstractions according to the requirements identified at design-time. We take as a representative for this scenario the logic-based language ReSpecT (Reaction Specification Tuples), used to program the reactive behaviour of tuple centres. ReSpecT specifications are at the core of the engineering methodology underlying the TuCSoN infrastructure, and are therefore the “conceptual place” where formal methods can be fruitfully applied to guarantee relevant system properties.In this paper we introduce ReSpecT nets, a formalism that can be used to describe reactive behaviours that can succeed and fail, and that allows for an encoding to Petri nets with inhibitor arcs. ReSpecT nets are introduced to give a core model to a fragment of the ReSpecT language, and to pave the way for devising an analysis methodology including formal verification of safety and liveness properties. In particular, we provide a semantics to ReSpecT specifications through a mapping to ReSpecT nets. The potential of this approach for the analysis of ReSpecT specifications is discussed, presenting initial results for the analysis of safety properties.     

Exogenous Probabilistic Computation Tree Logic

We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non–deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so–called quantum one–time pad.     

Stochastic Ambient Calculus

Mobile Ambients (MA) have acquired a fundamental role in modelling mobility in systems with mobile code and mobile devices, and in computation over administrative domains. We present the stochastic version of Mobile Ambients, called Stochastic Mobile Ambients (SMA), where we extend MA with time and probabilities. Inspired by previous models, PEPA and Sπ, we enhance the prefix of the capabilities with a rate and the ambient with a linear function that operates on the rates of processes executing inside it. The linear functions associated with ambients represent the delays that govern particular administrative domains. We derive performance measures from the labelled transition semantics as in standard models. We also define a strong Markov bisimulation in the style of reduction semantics known as barbed bisimulation. We argue that performance measures are of vital importance in designing any kind of distributed system, and that SMA can be useful in the design of the complicated mobile systems.     

PVS#: Streamlined Tacticals for PVS

The semantics of a proof language relies on the representation of the state of a proof after a logical rule has been applied. This information, which is usually meaningless from a logical point of view, is fundamental to describe the control mechanism of the proof search provided by the language. In this paper, we present a monadic datatype to represent the state information of a proof and we illustrate its use in the PVS theorem prover. We show how this representation can be used to design a new set of powerful tacticals for PVS, called PVS#, that have a simpler and clearer semantics compared to the semantics of standard PVS tacticals.     

A note on Rooted Survivable Networks

The (undirected) Rooted Survivable Network Design (Rooted SND) problem is: given a complete graph on node set V with edge-costs, a root sV, and (node-)connectivity requirements , find a minimum cost subgraph G that contains r(t) internally-disjoint st-paths for all tT. For large values of k=max_tTr(t) Rooted SND is at least as hard to approximate as Directed Steiner Tree [Y. Lando, Z. Nutov, Inapproximability of survivable networks, Theoret. Comput. Sci. 410 (21–23) (2009) 2122–2125]. For Rooted SND, [J. Chuzhoy, S. Khanna, Algorithms for single-source vertex-connectivity, in: FOCS, 2008, pp. 105–114] gave recently an approximation algorithm with ratio O(k²logn). Independently, and using different techniques, we obtained at the same time a simpler primal–dual algorithm with the same ratio.     

Virtual Organizations in Arigatoni

Arigatoni is a lightweight overlay network that deploys the Global Computing Paradigm over the Internet. Communication for over the behavioral units of the overlay is performed by a simple resource discovery protocol (RDP). Basic Global Computers Units (GC) can communicate by first registering to a brokering service and then by mutually asking and offering services.Colonies and communities are the main entities in the model. A colony is a simple virtual organization composed by exactly one leader and some set (possibly empty) of individuals. A community is a raw set of colonies and global computers (think it as a soup of colonies and global computer without a leader).We present an operational semantics via a labeled transition system, that describes the main operations necessary in the Arigatoni model to perform leader negotiation, joining/leaving a colony, linking two colonies and moving one GC from one colony to another. Our formalization results to be adequate w.r.t. the algorithm performing peer logging/delogging and colony aggregation.     

Designing a BPEL Orchestration Engine Based on ReSpecT Tuple Centres

We present the design of a BPEL orchestration engine based on ReSpecT tuple centres, a coordination model extending Linda with the ability of declaratively programming the reactive behaviour of tuple spaces. Architectural and linguistic aspects of our solution are discussed, focussing on how the syntax and semantics of BPEL have been mapped to tuple centres. This is achieved by a translation of BPEL specifications to set of logic tuples, and conceiving the execution cycle of the orchestration engine in terms of ReSpecT reactions.     

Wireless network design via 3-decompositions

We consider some network design problems with applications for wireless networks. The input for these problems is a metric space (X,d) and a finite subset UX of terminals. In the Steiner Tree with Minimum Number of Steiner Points (STMSP) problem, the goal is to find a minimum size set SX−U of points so that the unit-disc graph of S+U is connected. Let Δ be the smallest integer so that for any finite VX for which the unit-disc graph is connected, this graph contains a spanning tree with maximum degree Δ. The best known approximation ratio for STMSP was Δ−1 [I.I. Măndoiu, A.Z. Zelikovsky, A note on the MST heuristic for bounded edge-length Steiner trees with minimum number of Steiner points, Information Processing Letters 75 (4) (2000) 165–167]. We improve this ratio to (Δ+1)/2+1+ε.In the Minimum Power Spanning Tree (MPST) problem, V=X is finite, and the goal is to find a “range assignment” on the nodes so that the edge set contains a spanning tree, and ∑_vVp(v) is minimized. We consider a particular case {0,1}-MPST of MPST when the distances are in {0,1}; here the goal is to find a minimum size set SV of “active” nodes so that the graph (V,E₀+E₁(S)) is connected, where , and E₁(S) is the set the edges in with both endpoints in S. We will show that the (5/3+ε)-approximation scheme for MPST of [E. Althaus, G. Calinescu, I. Măndoiu, S. Prasad, N. Tchervenski, A. Zelikovsky, Power efficient range assignment for symmetric connectivity in static ad hoc wireless networks, Wireless Networks 12 (3) (2006) 287–299] achieves a ratio 3/2 for {0,1}-distances. This answers an open question posed in [E. Lloyd, R. Liu, S. Ravi, Approximating the minimum number of maximum power users in ad hoc networks, Mobile Networks and Applications 11 (2006) 129–142].     

Ordering the order of a distributive lattice by itself

We order the ordering relation of an arbitrary poset P component-wise by itself, obtaining a poset Φ(P) extending P. In particular, the effects of Φ on L  DLAT01, the category of all bounded distributive lattices, are studied, mainly with the aid of Priestley duality. We characterize those L  DLAT01 which occur as Φ(K) for some K  DLAT01, decide this situation in polynomial time for finite L, characterize fixpoints of Φ within DLAT01 and relate them to free objects in DLAT01.     

A connection between the Cantor–Bendixson derivative and the well-founded semantics of finite logic programs

Results of Schlipf (J Comput Syst Sci 51:64?C86, 1995) and Fitting (Theor Comput Sci 278:25?C51, 2001) show that the well-founded semantics of a finite predicate logic program can be quite complex. In this paper, we show that there is a close connection between the construction of the perfect kernel of a $\Pi^0_1$ class via the iteration of the Cantor?CBendixson derivative through the ordinals and the construction of the well-founded semantics for finite predicate logic programs via Van Gelder??s alternating fixpoint construction. This connection allows us to transfer known complexity results for the perfect kernel of $\Pi^0_1$ classes to give new complexity results for various questions about the well-founded semantics ${\mathit{wfs}}(P)$ of a finite predicate logic program P.     

A Language for Verification and Manipulation of Web Documents: (Extended Abstract)

In this paper we develop the language theory underpinning the logical framework PLF. This language features lambda abstraction with patterns and application via pattern-matching. Reductions are allowed in patterns. The framework is particularly suited as a metalanguage for encoding rewriting logics and logical systems where proof terms have a special syntactic constraints, as in term rewriting systems, and rule-based languages. PLF is a conservative extension of the well-known Edinburgh Logical Framework LF. Because of sophisticated pattern matching facilities PLF is suitable for verification and manipulation of HXML documents.     

From Chemical Rules to Term Rewriting

In this paper, rule-based programming is explored in the field of automated generation of chemical reaction mechanisms. We explore a class of graphs and a graph rewriting relation where vertices are preserved and only edges are changed. We show how to represent cyclic labeled graphs by decorated labeled trees or forests, then how to transform trees into terms. A graph rewriting relation is defined, then simulated by a tree rewriting relation, which can be in turn simulated by a rewriting relation on equivalence classes of terms. As a consequence, this kind of graph rewriting can be implemented using term rewriting. This study is motivated by the design of the GasEl system for the generation of kinetics reactions mechanisms. In GasEl, chemical reactions correspond to graph rewrite rules and are implemented by conditional rewriting rules in ELAN. The control of their application is done through the ELAN strategy language.     

A Simple Calculus for Proteins and Cells

The use of process calculi to represent biological systems has led to the design of different calculi such as brane calculi [Luca Cardelli. Brane calculi. In CMSB, pages 257–278, 2004] and κ-calculus [Vincent Danos and Cosimo Laneve. Formal molecular biology. Theoritical Computer Science, 325(1):69–110, 2004]. Both have proved to be useful to model different types of biological systems.As an attempt to unify the two directions, we introduce the bioκ-calculus, a simple calculus for describing proteins and cells, in which bonds are represented by means of shared names and interactions are modelled at the domain level. Protein-protein interactions have to be at most binary and cell interactions have to fit with sort constraints.We define the semantics of bioκ-calculus, analyse its properties, and discuss its expressiveness by modelling two significant examples: a signalling pathway and a virus infection.     

Linguistic$$\leftrightarrow $$Rational Agents’ Semantics

We define and prove a formal semantics divided into two complementary interacting components: the strictly linguistic (i.e. linguistically marked) semantics, we call linguistic agent (LA), and the strictly logical and referential semantics, we call rational agent (RA). This Linguistic \(\leftrightarrow \) Rational Agents’ Semantics (LRA semantics) applies to Deep Dependency trees (DD-trees) or more generally, to discourses, i.e. sequences of DD-trees, and interprets them by functional structures we call Meaning Representation Structures (MRS), similar to the DRT, but interpreted very differently. LRA semantics incrementally interprets the discourses by minimal finite models, called proto-models, in a monotonic logic of the LA and checks the proto-models with respect to the classical models of the RA. The proto-model is considered as the linguistic sense of the discourse. We define in full detail the LA which, as we believe, must be universal. On the other hand, we don’t propose a particular RA. We only define the scheme of interaction between the two agents and the stimuli of the RA used by the LA. After all, every discourse has in LRA semantics the single meaning and the single sense for every Rational Agent used to interact with the Linguistic Agent.     

In All But Finitely Many Possible Worlds: Model-Theoretic Investigations on ‘<Emphasis Type="Italic">Overwhelming Majority</Emphasis>’ Default Conditionals

Defeasible conditionals are statements of the form ‘if A then normally B’. One plausible interpretation introduced in nonmonotonic reasoning dictates that (\(A\Rightarrow B\)) is true iff B is true in ‘most’ A-worlds. In this paper, we investigate defeasible conditionals constructed upon a notion of ‘overwhelming majority’, defined as ‘truth in a cofinite subset of \(\omega \)’, the first infinite ordinal. One approach employs the modal logic of the frame \((\omega , <)\), used in the temporal logic of discrete linear time. We introduce and investigate conditionals, defined modally over \((\omega , <)\); several modal definitions of the conditional connective are examined, with an emphasis on the nonmonotonic ones. An alternative interpretation of ‘majority’ as sets cofinal (in \(\omega \)) rather than cofinite (subsets of \(\omega \)) is examined. For these modal approaches over \((\omega , <)\), a decision procedure readily emerges, as the modal logic \({\mathbf {K4DLZ}}\) of this frame is well-known and a translation of the conditional sentences can be mechanically checked for validity; this allows also for a quick proof of \(\mathsf {NP}\)-completeness of the satisfiability problem for these logics. A second approach employs the conditional version of Scott-Montague semantics, in the form of \(\omega \)-many possible worlds, endowed with neighborhoods populated by collections of cofinite subsets of \(\omega \). This approach gives rise to weak conditional logics, as expected. The relative strength of the conditionals introduced is compared to (the conditional logic ‘equivalent’ of) KLM logics and other conditional logics in the literature.     

Uniform provability realization of intuitionistic logic, modality and λ-terms

The intended meaning of intuitionistic logic is explained by the Brouwer-Heyting-Kolmogorov (BHK) provability semantics which informally defines intuitionistic truth as provability and specifies the intuitionistic connectives via operations on proofs. The problem of finding an adequate formalization of the provability semantics and establishing the completeness of the intuitionistic logic Int was first raised by Gödel in 1933. This question turned out to be a part of the more general problem of the intended realization for Gödel's modal logic of provability S4 which was open since 1933. In this tutorial talk we present a provability realization of Int and S4 that solves both of these problems. We describe the logic of explicit provability (LP) with the atoms “t is a proof of F” and establish that every theorem of S4 admits a reading in LP as the statement about operations on proofs. Moreover, both S4 and Int are shown to be complete with respect to this realization. In addition, LP subsumes the λ-calculus, modal λ-calculus, combinatory logic and provides a uniform provability realization of modality and λ-terms.     

Prototype Platforms for Distributed Agreements

We present a prototype application for coordinating distributed agreements in multi-parties negotiations, where participants can dynamically join ongoing negotiations and where participants know only those parties they have interacted with. Our prototype is tailored to Ad-Hoc network scenarios involving the assignment of tasks for a rescue team operating over disaster areas. Our application is based on asynchronous communication and it exploits the d2pc protocol for committing or aborting a negotiation. Parties have been developed both in Jocaml+Perl and Polyphonic C. The implementation of the commit protocol allows components of both types to participate within the same negotiation.