LAM'10: Papers with Abstracts

Abstract. Epistemic logic analyzes reasoning governing localized knowledge, and is thus fundamental to multi- agent systems. Linear logic treats hypotheses as consumable resources, allowing us to model evolution of state. Combining principles from these two separate traditions into a single coherent logic allows us to represent localized consumable resources and their flow in a distributed system. The slogan “possession is linear knowledge” summarizes the underlying idea. We walk through the design of a linear epistemic logic and discuss its basic metatheoretic properties such as cut elimination. We illustrate its expressive power with several examples drawn from an ongoing effort to design and implement a linear epistemic logic programming language for multi-agent distributed systems.

Abstract. The logic MBI is a substructural modal logic of locations, resources, and processes that is closely related to both the bunched logic BI and Hennessy-Milner logic. MBI stands in a (slightly weak) Hennessy-Milner correspondence with the synchronous process calculus of located resources, LSCRP. Starting from motivations in large-scale systems modelling, I will introduce MBI and LSCRP, and explain how they can be used to address some theoretical and practical questions in access control.

Abstract. We propose an approach to the quantitative modelling of crowd dy- namics, viz. the behaviour of systems of large numbers of mobile agents. The approach relies on a stochastic process algebra as specification lan- guage (BioPEPA), and combines stochastic simulation techniques and continuous fluid flow approximation. The approach encompasses the agent modelling viewpoint, as system behaviour emerges from the specified agent interaction, and the population modelling viewpoint, when continu- ous analysis is used. The result is expressive, as we will show by discussing a few examples, and efficient, by the adoption of the fluid flow analysis techniques, which approximate system dynamics as continuous variations of population.

Abstract. This contribution presents the formalism of ElementaryObjectSystems (Eos). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. One central aim of this contribution is to compile all our previous works ded- icated to certain aspects of Eos together with recent yet unpublished results within one self-contained presentation. Since object nets in general are immediately Turing complete, we introduce the restricted class of elementary object nets which restrict the nesting of nets to the depth of two. In this work we study the relationship of Eos to existing Petri net formalisms. It turns out that Eos are more powerful than classical p/t nets which is demonstrated by the fact that e.g. reachability and liveness become undecidable problems for Eos. Despite these undecidability results other properties can be extended to Eos using a monotonicity argument similar to that for p/t nets. Also linear algebraic techniques, especially the theory of linear invariants and semiflows, can be extended in an appropriate way. The invariant calculus for Eos even enjoys the property of compositionality, i.e. invariants of the whole system can be composed of invariants of the object nets, which reduces the computational effort. To obtain a finer level of insight we also studied several classes like pure, minimal, or semi-bounded Eos. Among these variants the subclass of generalised state machines is worth mentioning since it combines the decidability of many theoretically interesting properties with a quite rich practical modelling expressiveness.

Abstract. In this paper we discuss the complexity of LTL model checking of safe Elementary Object Nets (Eos). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-withinnets paradigm. Object nets are called elementary if the net system has a two levelled structure. The well known p/t nets can be considered as a special case of Eos. For p/t nets the concept of safeness means that there is at most one token on each place. Since object nets have nested markings there are different possibilities to generalise this idea for Eos. In this paper we concentrate on the variant of Eos safeness that guarantees the finiteness of state spaces and show that for safe Eos the LTL model checking problem is PSpace-complete.

Abstract. This paper demonstrates how a constructive version of the description logic ALC can serve as a semantic type system for an extension of the simply typed $\lambda$-calculus to express computations in knowledge bases. This cALculus embodies a functional core language which provides static type checking of semantic information for programming with data whose structure is organised under a relational data model. The cALculus arises from a natural interpretation of the tableau rules for constructive ALC following the Curry-Howard-Isomorphism.

Abstract. Network Datalog (<i>NDlog</i>) is a recursive query language that extends Datalog by allowing programs to be distributed in a network. In our initial efforts to formally specify <i>NDlog</i>'s operational semantics, we have found several problems with the current evaluation algorithm being used, including unsound results, unintended multiple derivations of the same table entry, and divergence. In this paper, we make a first step towards correcting these problems by formally specifying a new operational semantics for <i>NDlog</i> and proving its correctness for the fragment of non-recursive programs. We also argue that if termination is guaranteed, then the results also extend to recursive programs. Finally, we identify a number of potential implementation improvements to <i>NDlog</i>.

Abstract. We develop an algebraic modal logic that combines epistemic and dynamic modalities with a view to modelling information acquisition (learning) by automated agents in a changing world. Unlike most treatments of dynamic epistemic logic, we have transitions that ``change the state'' of the underlying system and not just the state of knowledge of the agents. The key novel feature that emerges is the need to have a way of ``inverting transitions'' and distinguishing between transitions that ``really happen'' and transitions that are possible.

Our approach is algebraic, rather than being based on a Kripke-style semantics. The semantics are given in terms of quantales. We introduce a class of quantales with the appropriate inverse operations and use it to model toy robot-navigation problems, which illustrate how an agent learns information by taking actions. We discuss how a sound and complete logic of the algebra may be obtained from the positive fragment of PDL with converse.

Abstract. Web applications (webapps) are very popular because they are easy to prototype and they can make use of other webapps, supplied by third parties, as building blocks. Yet, writing correct webapps is complex because developers are required to reason about distributed computation and to write code using heterogeneous languages, often not originally designed with distributed computing in mind. Testing is the common way to catch bugs as current technologies provide limited support. There are doubts this can scale up to meet the expectations of more sophisticated web applications. In this paper, we propose an abstraction that provides simple primitives to manage the two main forms of distributed computation found on the web: remote procedure calls (code executed on a server on behalf of a client) and mobile code (server code executed on a client). We embody this abstraction in a type-safe language with localized static typechecking that we call QWeSST and for which we have implemented a working prototype. We use it to express interaction patterns commonly found on the Web as well more sophisticated forms that are beyond current web technologies.