Author name cluster

Bengt Jonsson

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers

1 author row

TCS Journal 2014 Journal Article

An algebraic theory of interface automata

Chris Chilton
Bengt Jonsson
Marta Kwiatkowska

We formulate a compositional specification theory for interface automata, where a component model specifies the allowed sequences of input and output interactions with the environment. A trace-based linear-time refinement is provided, which is the weakest preorder preserving substitutivity of components, and is weaker than the classical alternating simulation defined on interface automata. Since our refinement allows a component to be refined by refusing to produce any output, we also define a refinement relation that guarantees safety and progress. The theory includes the operations of parallel composition to support the structural composition of components, logical conjunction and disjunction for independent development, hiding to support abstraction of interfaces, and quotient for incremental synthesis of components. Our component formulation highlights the algebraic properties of the specification theory for both refinement preorders, and is shown to be fully abstract with respect to observation of communication mismatches. Examples of independent and incremental component development are provided.

Details DOI

TCS Journal 2010 Journal Article

Learning of event-recording automata

Olga Grinchtein
Bengt Jonsson
Martin Leucker

In regular inference, a regular language is inferred from answers to a finite set of membership queries, each of which asks whether the language contains a certain word. One of the most well-known regular inference algorithms is the L ∗ algorithm due to Dana Angluin. However, there are almost no extensions of these algorithms to the setting of timed systems. We extend Angluin’s algorithm for on-line learning of regular languages to the setting of timed systems. Since timed automata can freely use an arbitrary number of clocks, we restrict our attention to systems that can be described by deterministic event-recording automata (DERAs). We present three algorithms, T L s g ∗, T L n s g ∗ and T L s ∗, for inference of DERAs. In T L s g ∗ and T L n s g ∗, we further restrict event-recording automata to be event-deterministic in the sense that each state has at most one outgoing transition per action; learning such an automaton becomes significantly more tractable. The algorithm T L n s g ∗ builds on T L s g ∗, by attempts to construct a smaller (in number of locations) automaton. Finally, T L s ∗ is a learning algorithm for a full class of deterministic event-recording automata, which infers a so called simple DERA, which is similar in spirit to the region graph.

Details DOI

I&C Journal 2005 Journal Article

Simulating perfect channels with probabilistic lossy channels

Parosh Abdulla
Christel Baier
S. Purushothaman Iyer
Bengt Jonsson

We consider the problem of deciding whether an infinite-state system (expressed as a Markov chain) satisfies a correctness property with probability 1. This problem is, of course, undecidable for general infinite-state systems. We focus our attention on the model of probabilistic lossy channel systems consisting of finite-state processes that communicate over unbounded lossy FIFO channels. Abdulla and Jonsson have shown that safety properties are decidable while progress properties are undecidable for non-probabilistic lossy channel systems. Under assumptions of “sufficiently high” probability of loss, Baier and Engelen have shown how to check whether a property holds of probabilistic lossy channel system with probability 1. In this paper, we consider a model of probabilistic lossy channel systems, where messages can be lost only during send transitions. In contrast to the model of Baier and Engelen, once a message is successfully sent to channel, it can only be removed through a transition which receives the message. We show that checking whether safety properties hold with probability 1 is undecidable for this model. Our proof depends upon simulating a perfect channel, with a high degree of confidence, using lossy channels.

Details DOI

TCS Journal 2003 Journal Article

Model checking of systems with many identical timed processes

Parosh Aziz Abdulla
Bengt Jonsson

Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid̈ automata, data-independent systems, relational automata, Petri nets, lossy channel systems, context-free and push-down processes. We present a method for deciding reachability properties of networks of timed processes. Such a network consists of an arbitrary set of identical timed automata, each with a single real-valued clock. Using a standard reduction from safety properties to reachability properties, we can use our algorithm to decide general safety properties of timed networks. To our knowledge, this is the first decidability result concerning verification of systems that are infinite-state in “two dimensions”: they contain an arbitrary set of (identical) processes, and they use infinite data-structures, viz real-valued clocks. We illustrate our method by showing how it can be used to automatically verify Fischer's protocol, a timer-based protocol for enforcing mutual exclusion among an arbitrary number of processes. Finally, we show undecidability of the recurrent state problem: given a state in a timed network, check whether there is a computation of the network visiting the state infinitely often. This implies undecidability of model checking for any temporal logic which is sufficiently expressive to encode the recurrent state problem, such as PTL, CTL, etc.

Details DOI

TCS Journal 2002 Journal Article

Testing preorders for probabilistic processes can be characterized by simulations

Bengt Jonsson
Wang Yi

Transition systems are well established as a semantic model for distributed systems. There are several preorders that serve as criteria for refinement of an abstract transition system to a more concrete one. To reason about probabilistic phenomena such as failures and randomization, we need to extend models and methods that have proven successful for nonprobabilistic systems to a probabilistic setting. In this paper, we develop a refinement preorder for a probabilistic extension of the transition systems model. The preorder is based on a notion of testing, where refinement corresponds to an improvement in the “worst-case” behavior of a process. The main result of the paper is that this preorder can be described by a notion of probabilistic simulation, which generalizes the standard simulation preorder for ordinary transition system. To our knowledge, this simulation preorder has not been previously described in the literature, and is strictly weaker than previously proposed simulations for probabilistic transition systems.

Details DOI

TCS Journal 2001 Journal Article

Ensuring completeness of symbolic verification methods for infinite-state systems

Parosh Aziz Abdulla
Bengt Jonsson

Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. For different classes of such systems, e. g. , hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems, this research has resulted in numerous highly nontrivial algorithms. As the interest in this area increases, it will be important to extract common principles that underly these and related results. In this paper, we will present a general model of infinite-state systems, and describe a standard algorithm for reachability analysis of such systems. Our contribution consists in finding conditions under which the algorithm can be fully automated. We perform backward reachability analysis. Using an iterative procedure, we generate successively larger approximations of the set of all states from which a given final state is reachable. We consider classes of systems where these approximations are well quasi-ordered, implying that the iterative procedure always terminates. Starting from these general termination conditions, we derive several computations models for which reachability is decidable. Many of these models are extensions of those existing in the literature. Using a well-known reduction from safety properties to reachability properties, we can use our algorithm to decide large classes of safety properties for infinite-state systems. A motivation for our approach is the long-term desire to build general tools for verification of infinite-state systems, which implies that we should employ principles applicable across a rather wide range of such systems.

Details DOI

I&C Journal 2000 Journal Article

Algorithmic Analysis of Programs with Well Quasi-ordered Domains

Parosh Aziz Abdulla
Kārlis Čerāns
Bengt Jonsson
Yih-Kuen Tsay

Over the past few years increasing research effort has been directed towards the automatic verification of infinite-state systems. This paper is concerned with identifying general mathematical structures which can serve as sufficient conditions for achieving decidability. We present decidability results for a class of systems (called well-structured systems) which consist of a finite control part operating on an infinite data domain. The results assume that the data domain is equipped with a preorder which is a well quasi-ordering, such that the transition relation is “monotonic” (a simulation) with respect to the preorder. We show that the following properties are decidable for well-structured systems: • Reachability: whether a certain set of control states is reachable. Other safety properties can be reduced to the reachability problem. • Eventuality: whether all executions eventually reach a given set of control states (represented as AFp in CTL). • Simulation: whether there exists a simulation between a finite automaton and a well-structured system. The simulation problem will be shown to be decidable in both directions. We also describe how these general principles subsume several decidability results from the literature about timed automata, relational automata, Petri nets, and lossy channel systems.

Details DOI

I&C Journal 1998 Journal Article

A Fully Abstract Semantics for Concurrent Constraint Programming

Sven-Olof Nyström
Bengt Jonsson

A compositional and fully abstract semantics for concurrent constraint programming is developed. It is the first fully abstract semantics which takes into account both non-determinism, infinite computations, and fairness. We present a simple concurrent constraint programming language, whose semantics is given by a set of reduction rules augmented with fairness requirements. In the fully abstract semantics we consider two aspects of a trace, viz. the function computed by the trace (the functionality) and the set of input and output data (the limit of the trace). We then derive the fully abstract semantics from the set of traces using a closure operation. We give two proofs of full abstraction; the first relies on the use of a syntactically infinite context. The second proof requires only a finite context, but assumes as input a representation of the function to be computed by the context. Finally, we examine the algebraic properties of the programming language with respect to the fully abstract semantics. It turns out that the non-deterministic selection operation can be defined using operations derived from parallel composition and the usual set-theoretic operations on sets of traces.

Details DOI

TCS Journal 1996 Journal Article

Assumption/guarantee specifications in linear-time temporal logic

Bengt Jonsson
Tsay Yih-Kuen

An assumption/guarantee specification of a system consists of an assumption part, which specifies the assumptions on the behavior of the environment, and a guarantee part, which specifies the properties guaranteed by the system if the environment obeys the assumptions. A suitable interpretation of an assumption/guarantee specification was essentially formulated by Misra and Chandy (1981). The interpretation was later extended by others to allow liveness properties in the guarantee part. In this paper, we explore the use of linear-time temporal logic in writing and reasoning about assumption/guarantee specifications. We choose this logic, specifically LTL defined in the book by Manna and Pnueli (1992), for the following reasons: (i) Linear-time temporal logics, including LTL and TLA, have proven to be a successful formalism for the specification and verification of concurrent systems. (ii) Previous works on assumption/guarantee specifications typically reason about relevant properties at the semantic level or define a special-purpose logic. We feel it is beneficial to formulate such specifications in a more widely used formalism. (iii) We find that, with past temporal operators, LTL admits a succinct syntactic formulation of assumption/guarantee specifications. This contrasts, in particular, with the work by Abadi and Lamport using TLA, where working at the syntactic level is more complicated. We derive inference rules for refining and composing assumption/guarantee specifications as the main results of this paper. The derived rules can handle internal variables. We had to overcome a number of technical problems in this pursuit, in particular, the problem of extracting the safety closure of a temporal formula. As a by-product, we identify general conditions under which the safety closure can be expressed in a succinct way that facilitates syntactic manipulation.

Details DOI

I&C Journal 1996 Journal Article

Undecidable Verification Problems for Programs with Unreliable Channels

Parosh Aziz Abdulla
Bengt Jonsson

We consider the class of finite-state systems communicating through unbounded butlossyFIFO channels (calledlossy channel systems). These systems have infinite state spaces due to the unboundedness of the channels. In an earlier paper, we showed that the problems of checking reachability, safety properties, and eventuality properties are decidable for lossy channel systems. In this paper, we show that the following problems are undecidable: •The model checking problem in propositional temporal logics such as propositional linear time temporal logic (PTL) and computation tree logic (CTL). •The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels satisfy fairness assumptions? The results are obtained through reduction from a variant of the Post correspondence problem.

Details DOI

I&C Journal 1996 Journal Article

Verifying Programs with Unreliable Channels

Parosh Aziz Abdulla
Bengt Jonsson

We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model, e. g. , link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, we show that several interesting verification problems are decidable by giving algorithms for verifying (1) thereachability problem—is a finite set of global states reachable from some other global state of the system? (2)safety properties over tracesformulated as regular sets of allowed finite traces, and (3)eventuality properties—do all computations of a system eventually reach a given set of states? We have used the algorithms to verify some idealized sliding-window protocols with reasonable time and space resources. Our results should be contrasted with the well-known fact that these problems are undecidable for systems with unboundedperfectFIFO channels.

Details DOI