Expressing Priorities and External Probabilities in Process Algebra via Mixed Open/Closed Systems

Defining operational semantics for a process algebra is often based either on labeled transition systems that account for interaction with a context or on the so-called reduction semantics: we assume to have a representation of the whole system and we compute unlabeled reduction transitions (leading to a distribution over states in the probabilistic case). In this paper we consider mixed models with states where the system is still open (towards interaction with a context) and states where the system is already closed. The idea is that (open) parts of a system “P” can be closed via an operator “P↑G” that turns already synchronized actions whose “handle” is specified inside “G” into prioritized reduction transitions (and, therefore, states performing them into closed states). We show that we can use the operator “P↑G” to express multi-level priorities and external probabilistic choices (by assigning weights to handles inside G), and that, by considering reduction transitions as the only unobservable τ transitions, the proposed technique is compatible, for process algebra with general recursion, with both standard (probabilistic) observational congruence and a notion of equivalence which aggregates reduction transitions in a (much more aggregating) trace based manner. We also observe that the trace-based aggregated transition system can be obtained directly in operational semantics and we present the “aggregating” semantics. Finally, we discuss how the open/closed approach can be used to also express discrete and continuous (exponential probabilistic) time and we show that, in such timed contexts, the trace-based equivalence can aggregate more with respect to traditional lumping based equivalences over Markov Chains.     

A View on Decoherence Via Master Equations

This paper addresses the discussion on probabilistic features of the concept of decoherence as it appeared in quantum physics. Given a Lindblad-type generator of an open system dynamics, we derive applicable criteria to characterize decoherent behaviour.Presented at the International Conference “Entanglement, Information & Noise”, Krzyżowa, Poland, June 14-20, 2004.Partially supported by FONDECYT grant 1030552.     

Description of Quantum Dynamics of Open Systems Based on Collision-Like Models

Master equations in the Lindblad form describe evolution of open quantum systems that are completely positive and simultaneously have a semigroup property. We analyze the possibility to derive this type of master equations from an intrinsically discrete dynamics that is modelled as a sequence of collisions between a given quantum system (a qubit) with particles that form the environment. In order to illustrate our approach we analyze in detail how the process of an exponential decay and the process of decoherence can be derived from a collision-like model in which particular collisions are described by SWAP and controlled-NOT interactions, respectively.Presented at the 36th Symposium on Mathematical Physics, “Open Systems & Quantum Information”, Toruń, Poland, June 9-12, 2004.     

Non-Decomposable Quantum Dynamical Semigroups and Bound Entangled States

We use open quantum system techniques to construct one-parameter semigroups of positive maps and apply them to study the entanglement properties of a class of 16-dimensional density matrices, representing states of a 4 × 4 bipartite system.Presented at the International Conference “Entanglement, Information & Noise”, Krzyżowa, Poland, June 14–20, 2004.     

Towards coalgebraic behaviourism

In this paper we show that it is possible to model observable behaviour of coalgebras independently from their internal dynamics, but within the general framework of representing behaviour by a map into a “final” coalgebra.In the first part of the paper we characterise Set-endofunctors F with the property that bisimilarity of elements of F-coalgebras coincides with having the same observable behaviour. We show that such functors have the final coalgebra of a rather simple nature, and preserve some weak pullbacks. We also show that this is the case if and only if F-bisimilarity corresponds to logical equivalence in the finitary fragment of the coalgebraic logic.In the second part of the paper, we present a construction of a “final” coalgebra that captures the observable behaviour of F-coalgebras. We keep the word “final” quoted since the object we are going to construct need not belong to the original category. The construction is carried out for arbitrary Set-endofunctor F, throughout the construction we remain in Set, but the price to pay is the introduction of new morphisms. The paper concludes with a hint to a possible application to modelling weak bisimilarity for coalgebras.     

A Proof Search Specification of the π-Calculus

We present a meta-logic that contains a new quantifier (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.     

A Temporal Logic for Proving Properties of Topologically General Executions

We present a generalization of the temporal propositional logic of linear time which is useful for stating and proving properties of the generic execution sequence of a parallel program or a non-deterministic program. The formal system we present is exactly that same as the third of three logics presented by Lehmann and Shelah (Information and Control53, 165–198 (1982)), but we give it a different semantics. The models are tree models of arbitrary size similar to those used in branching time temporal logic. The formulation we use allows us to state properties of the “co-meagre” family of paths, where the term “co-meagre” refers to a set whose complement is of the first category in Baire's classification looking at the set of paths in the model as a metric space. Our system is decidable, sound, and, complete for models of arbitrary size, but it has the finite model property; namely, every sentence having a model has a finite model.     

A framework for specifying and verifying the behaviour of open systems

Coding no longer represents the main issue in developing software applications. It is the design and verification of complex software systems that require to be addressed at the architectural level, following methodologies which permit us to clearly identify and design the components of a system, to understand precisely their interactions, and to formally verify the properties of the systems. Moreover, this process is made even more complicated by the advent of the “network-centric” model of computation, where open systems dynamically interact with each other in a highly volatile environment. Many of the techniques traditionally used for closed systems are inadequate in this context.We illustrate how the problem of modeling and verifying behavioural properties of open system is addressed by different research fields and how their results may contribute to a common solution. Building on this, we propose a methodology for modeling and verifying behavioural aspects of open systems. We introduce the IP-calculus, derived from the π-calculas process algebra so as to describe behavioural features of open systems. We define a notion of partial correctness, acceptability, in order to deal with the intrinsic indeterminacy of open systems, and we provide an algorithmic procedure for its effective verification.     

First-Order Logic with Two Variables and Unary Temporal Logic

We investigate the power of first-order logic with only two variables over ω-words and finite words, a logic denoted by FO². We prove that FO² can express precisely the same properties as linear temporal logic with only the unary temporal operators: “next,” “previously,” “sometime in the future,” and “sometime in the past,” a logic we denote by unary-TL Moreover, our translation from FO² to unary-TL converts every FO² formula to an equivalent unary-TL formula that is at most exponentially larger and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is essentially optimal. While satisfiability for full linear temporal logic, as well as for unary-TL, is known to be PSPACE-complete, we prove that satisfiability for FO² is NEXP-complete, in sharp contrast to the fact that satisfiability for FO³ has nonelementary computational complexity. Our NEXP upper bound for FO² satisfiability has the advantage of being in terms of the quantifier depth of the input formula. It is obtained using a small model property for FO² of independent interest, namely, a satisfiable FO² formula has a model whose size is at most exponential in the quantifier depth of the formula. Using our translation from FO² to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.     

Specification in CTL+Past for Verification in CTL

We describe PCTL, a temporal logic extending CTL with connectives allowing to refer to the past of a current state. This incorporates the new N, “from now on,” combinator we recently introduced. PCTL has a branching future, but a determined, finite, and cumulative past. We argue this is the right choice for a semantical framework and show this through an extensive example. We investigate the feasibility of verification with PCTL and demonstrate how a translation-based approach allows model-checking specifications written in NCTL, a fragment of PCTL.     

Preprocessing of Intractable Problems

Some computationally hard problems, e.g., deduction in logical knowledge bases– are such that part of an instance is known well before the rest of it, and remains the same for several subsequent instances of the problem. In these cases, it is useful to preprocess off-line this known part so as to simplify the remaining on-line problem. In this paper we investigate such a technique in the context of intractable, i.e., NP-hard, problems. Recent results in the literature show that not all NP-hard problems behave in the same way: for some of them preprocessing yields polynomial-time on-line simplified problems (we call them compilable), while for other ones their compilability implies some consequences that are considered unlikely. Our primary goal is to provide a sound methodology that can be used to either prove or disprove that a problem is compilable. To this end, we define new models of computation, complexity classes, and reductions. We find complete problems for such classes, “completeness” meaning they are “the less likely to be compilable.” We also investigate preprocessing that does not yield polynomial-time on-line algorithms, but generically “decreases” complexity. This leads us to define “hierarchies of compilability,” that are the analog of the polynomial hierarchy. A detailed comparison of our framework to the idea of “parameterized tractability” shows the differences between the two approaches.     

Stabilized Moving Finite Elements for Convection Dominated Problems

The Moving Finite Element method (MFE) when applied to purely hyperbolic problems tends to move its nodes with the flow (often a good thing). But for steady or near steady problems the nodes flow past stationary regions of critical interest and pile up at the outflow. We report on efforts to develop moveable node versions of the “stabilized” finite element methods which have so successfully improved upon Galerkin in the fixed node setting. One method in particular (Galerkin-Δx TLSMFE with a “fix”) yields very promising results on our simple 1-D model problem. Its nodes lock onto and resolve sharp stationary features but also lock onto and move with the moving features of the solution.     

Dynamic learning from multiple examples for semantic object segmentation and search

We present a novel “dynamic learning” approach for an intelligent image database system to automatically improve object segmentation and labeling without user intervention, as new examples become available, for object-based indexing. The proposed approach is an extension of our earlier work on “learning by example,” which addressed labeling of similar objects in a set of database images based on a single example. The proposed dynamic learning procedure utilizes multiple example object templates to improve the accuracy of existing object segmentations and labels. Multiple example templates may be images of the same object from different viewing angles, or images of related objects. This paper also introduces a new shape similarity metric called normalized area of symmetric differences (NASD), which has desired properties for use in the proposed “dynamic learning” scheme, and is more robust against boundary noise that results from automatic image segmentation. Performance of the dynamic learning procedures has been demonstrated by experimental results.     

A logic for reasoning about probabilities

We consider a language for reasoning about probability which allows us to make statements such as “the probability of E₁ is less than ” and “the probability of E₁ is at least twice the probability of E₂,” where E₁ and E₂ are arbitrary events. We consider the case where all events are measurable (i.e., represent measurable sets) and the more general case, which is also of interest in practice, where they may not be measurable. The measurable case is essentially a formalization of (the propositional fragment of) Nilsson's probabilistic logic. As we show elsewhere, the general (nonmeasurable) case corresponds precisely to replacing probability measures by Dempster-Shafer belief functions. In both cases, we provide a complete axiomatization and show that the problem of deciding satisfiability is NP-complete, no worse than that of propositional logic. As a tool for proving our complete axiomatizations, we give a complete axiomatization for reasoning about Boolean combinations of linear inequalities, which is of independent interest. This proof and others make crucial use of results from the theory of linear programming. We then extend the language to allow reasoning about conditional probability and show that the resulting logic is decidable and completely axiomatizable, by making use of the theory of real closed fields.     

Control design for recycled, multi unit processes

An integrated multi-unit chemical plant presents a challenging control design problem due to the existence of recycling streams. In this paper, we develop a framework for analyzing the effects of recycling dynamics on closed-loop performance from which a systematic design of a decentralized control system for a recycled, multi-unit plant is established. In the proposed approach, the recycled streams are treated as unmodelled dynamics of the “unit” model so that their effects on closed-loop stability and performance can be analyzed using the robust control theory. As a result, two measures are produced: (1) the ν-gap metric, which quantifies the strength of recycling effects, and (2) the maximum stability margin of “unit” controller, which represents the ability of the “unit” controller to compensate for such effects. A simple rule for the “unit” control design is then established using the combined two measures in order to guarantee the attainment of good overall closed-loop performances. As illustrated by several design examples, the controllability of a recycled, multi unit process under a decentralized “unit” controller can be determined without requiring any detailed design of the “unit” controller because the simple rule is calculated from the open-loop information only.     

Internal stabilizability of the Navier–Stokes equations

One shows that the steady-state solutions to Navier–Stokes equations in d-dimensional domains Ω, d=2,3 with Dirichlet and slip curl boundary conditions are exponentially stabilizable by proportional controllers with the support in open subsets ωΩ such that Ωω is sufficiently “small”.     

A Coalgebraic Semantics for Epistemic Programs

This paper gives a fresh look at my previous work on “epistemic actions” and information updates in distributed systems, from a coalgebraic perspective. I show that the “relational” semantics of epistemic programs, given in [BMS2] in terms of epistemic updates, can be understood in terms of functors on the category of coalgebras and natural transformations associated to them. Then, I introduce a new, alternative, more refined semantics for epistemic programs: programs as “epistemic coalgebras”. I argue for the advantages of this second semantics, from a semantic, heuristic, syntactical and proof-theoretic point of view. Finally, as a step towards a generalization, I show these concepts make sense for other functors, and that apparently unrelated concepts, such as Bayesian belief updates and process transformations, can be seen to arise in the same way as our “epistemic actions”.     

Collecting Statistics over Runtime Executions

By collecting statistics over runtime executions of a program we can answer complex queries, such as “what is the average number of packet retransmissions” in a communication protocol, or “how often does process P₁ enter the critical section while process P₂ waits” in a mutual exclusion algorithm. We present an extension to linear-time temporal logic that combines the temporal specification with the collection of statistical data. By translating formulas of this language to alternating automata we obtain a simple and efficient query evaluation algorithm. We illustrate our approach with examples and experimental results.