Bengt Jonsson

Regular Inference for Communication Protocol Entities (2009)

Therese Bohlin, Bengt Jonsson

Abstract. Existing algorithms for regular inference (aka automata learning) allows to infer a finite state machine model of a system under test (SUT) by observing the output that the SUT produces in...

Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols (Extended Version) (2009)

Mayank Saksena, Oskar Wibling, Bengt Jonsson

Abstract. We present a technique for modeling and automatic verification of network protocols, based on graph transformation. It is suitable for protocols with a potentially unbounded number of...

A Divide-and-Conquer Strategy for Regular Model Checking (2009)

Bengt Jonsson, Ahmed Rezine, Mayank Saksena

Abstract. Regular model checking is being developed for algorithmic verification of several classes of infinite-state systems whose configurations can be modeled as words over a finite alphabet....

CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems (2009)

Issarny, Valérie, Steffen, Bernhard, Jonsson, Bengt, Blair, Gordon, Grace, Paul, Kwiatkowska, Marta, ...

The CONNECT European project that started in February 2009 aims at dropping the interoperability barrier faced by today's distributed systems. It does so by adopting a revolutionary approach to the...

CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems (2009)

Issarny, Valérie, Steffen, Bernhard, Jonsson, Bengt, Blair, Gordon, Grace, Paul, Kwiatkowska, Marta, ...

The CONNECT European project that started in February 2009 aims at dropping the interoperability barrier faced by today's distributed systems. It does so by adopting a revolutionary approach to the...

Multicore computing--the state of the art (2008)

Bengtsson, Christer, Brorsson, Mats, Grahn, Håkan, Hagersten, Erik, Jonsson, Bengt, ...

This document presents the current state of the art in multicore computing, in hardware and software, as well as ongoing activities, especially in Sweden. To a large extent, it draws on the...

REVIEWS (2008)

J Work, Environ Health, Bengt Jonsson, Asa Kilborn, Ilkka Aa Kuorinka, Barbara A Silverstein, ...

A conceptual model for work-related neck and upper-limb musculoskeletal disorders

Model-based Testing of Reactive Systems A Seminar Volume 19 Model checking (2008)

Manfred Broy, Bengt Jonsson, Joost-pieter Katoen, Martin Leucker, Alexander Pretschner (eds, Therese Berg, ...

When developing hard- or software systems one starts with a collection of requirements. Most requirements arise due to the needs of the customer, others originate from design decisions and further...

Systematic Acceleration in Regular Model Checking (2008)

Bengt Jonsson, Mayank Saksena

Abstract. Regular model checking is a form of symbolic model checking technique for systems whose states can be represented as finite words over a finite alphabet, where regular sets are used as...

University. Industrial contact (2008)

Bengt Jonsson, Ulf Wiger, Ericsson Telecom Ab, Thomas Arts

ERLANG is a concurrent functional language, which has been successfully used for the development of complex telecommunication software within Ericsson. An important feature of ERLANG, which allows to...

Abstract INFINITY 2004 Preliminary Version Inference of Timed Transition Systems (2008)

Olga Grinchtein, Bengt Jonsson, Martin Leucker

We extend Angluin’s algorithm for on-line learning of regular languages to the setting of timed transition systems. More specifically, we describe a procedure for inferring systems that can be...

INFINITY 2004 Preliminary Version (2008)

Inference Of Timed, Olga Grinchtein, Bengt Jonsson, Martin Leucker

We extend Angluin's algorithm for on-line learning of regular languages to the setting of timed transition systems. More specifically, we describe a procedure for inferring systems that can be...

2 (2007)

Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili

Abstract. We present regular model checking, a framework for algorithmic verification of infinite-state systems with, e.g., queues, stacks, integers, or a parameterized linear topology. States are...

Regular Model Checking made Simple and (2007)

Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson

Abstract. We present a new technique for computing the transitive closure of a regular relation characterized by a nite-state transducer. The construction starts from the original transducer, and...

Undecidability of reasoning about probabilistic lossy channel systems (2007)

Parosh Abdulla, Christel Baier, Purushothaman Iyer, Bengt Jonsson

We consider the problem of deciding whether an innite-state system (expressed as a Markov chain) satises a correctness property with probability 1. This problem is, of course, undecidable for general...

Automated Generation of Test Oracles from Temporal Logic SPecifications (2007)

John Hakansson, Bengt Jonsson, Ola Lundkvist

In current software development technology, testing is the dominant form of validation and verification of software products. In current practive, testing is performed with a rather low degree of...

Extracting the processes structure of Erlang applications (2007)

Bengt Jonsson

Erlang is a concurrent functional language, especially tailored for distributed and fault-tolerant software. Its strength has been demonstrated by several successful commercial applications. An...

Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) Generating On-Line Test Oracles from Temporal Logic Specications (2007)

Bengt Jonsson, Ola Lundqvist

Abstract. The paper concerns testing as a technique to check that a software component satis-es a specication of safety properties. In testing there must be some procedure, often called a test...

Modeling and Automated Verification of Authentication Protocols (2007)

Parosh Aziz Abdulla, Bengt Jonsson

In this paper we present a general framework for modeling infinite-state authentication protocols that allows an unbounded number of protocol participants. We present a method for automated...

A Case Study in Automated Detection of Service Interaction y (2007)

Gustaf Naeser, Jan Nystrom, Bengt Jonsson

This paper describes a case study in automated detection of service interaction (or service interference). We present an implemented system, which takes as input a set of services, between which...

Building Tools for Creation and Analysis of Telephone Services y (2007)

Gustaf Naeser, Jan Nystrom, Bengt Jonsson

This paper describes ongoing work on howto make a coherent framework for the creation of telephone services. The demands on the framework is that it should be easy to design, simulate and validate...

El aprendizaje autónomo de lenguas en tándem : principios, estrategias y experiencias de integración (2006)

Brammerts, Helmunt, Little, David, Calvert, Mike, John, Elke St., White, Liz, Woodin, Jane, ...

Recopilación de artículos dirigidos a profesores de lenguas, asesores lingüísticos y a aquellos que deseen organizar y apoyar el aprendizaje autónomo de lenguas en tándem. Se recogen las...

Regular inference for state machines with parameters (2006)

Therese Berg, Bengt Jonsson, Harald Raffelt

Abstract. Techniques for inferring a regular language, in the form of a finite automaton, from a sufficiently large sample of accepted and nonaccepted input words, have been employed to construct...

Proving Liveness by Backwards Reachability (2006)

Parosh Aziz Abdulla, Bengt Jonsson, Ahmed Rezine, Mayank Saksena

Abstract. We present a new method for proving liveness and termination properties for fair concurrent programs, which does not rely on finding a ranking function or on computing the transitive...

Inference of eventrecording automata using timed decision trees (2006)

Olga Grinchtein, Bengt Jonsson

In regular inference, the problem is to infer a regular language, typically represented by a deterministic finite automaton (DFA) from answers to a finite set of membership queries, each of which...

Specifying and Generating Test Cases Using Observer Automata (2005)

Johan Blom, Anders Hessel, Bengt Jonsson, Paul Pettersson

Abstract. We present a technique for specifying coverage criteria and a method for generating test suites for systems whose behaviours can be described as extended finite state machines (EFSM). To...

On the correspondence between conformance testing and regular inference (2005)

Therese Berg, Olga Grinchtein, Bengt Jonsson, Martin Leucker, Harald Raffelt, Bernhard Steffen

Abstract. Conformance testing for finite state machines and regular inference both aim at identifying the model structure underlying a black box system on the basis of a limited set of observations....

On the correspondence between conformance testing and regular inference (2005)

Therese Berg, Olga Grinchtein, Bengt Jonsson, Martin Leucker, Harald Raffelt, Bernhard Steffen

Abstract. Conformance testing for finite state machines and regular inference both aim at identifying the model structure underlying a black box system on the basis of a limited set of observations....

Using forward reachability analysis for verification of lossy channel systems (2004)

Parosh Aziz Abdulla, Aurore Annichini, Ahmed Bouajjani, Bengt Jonsson

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel...

Learning of Event-Recording Automata (2004)

Olga Grinchtein Bengt, Bengt Jonsson, Martin Leucker

We extend Angluin's algorithm for on-line learning of regular languages to the setting of timed systems. We consider systems that can be described by a class of deterministic event-recording...

Learning of event-recording automata (2004)

Olga Grinchtein, Bengt Jonsson, Martin Leucker

Abstract. We extend Angluin’s algorithm for on-line learning of regular languages to the setting of timed systems. We consider systems that can be described by a class of deterministic...

A survey of regular model checking (2004)

Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Mayank Saksena

Abstract. Regular model checking is being developed for algorithmic verification of several classes of infinite-state systems whose configurations can be modeled as words over a finite alphabet....

Learning of event-recording automata (2004)

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...

Algorithmic improvements in regular model checking (2003)

Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson

Abstract. Regular model checking is a form of symbolic model checking for parameterized and innite-state systems, whose states can be represented as nite strings of arbitrary length over a nite...

Insights to Angluin’s learning (2003)

Therese Berg, Bengt Jonsson, Martin Leucker, Mayank Saksena

Abstract. Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied....

Automated Test Generation for Industrial Erlang Applications (2003)

Johan Blom, Bengt Jonsson

We present an implemented technique for generating test cases from state machine specifications. The work is motivated by a need for testing of protocols and services developed by the company Mobile...

Http://www.artist-Embedded.org/ (2003)

Geoff Coulson, Ivica Crnkovic, Andy Evans, Sébastien Gérard, Susanne Graf, ...

this document, we survey the use of component technologies in di#erent industrial sectors. Two important obstacles to wider adoption of component technology for real-time systems are the following

Insights to Angluin's Learning (2003)

Therese Berg, Bengt Jonsson, Martin Leucker, Mayank Saksena

Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied.

of collaboration between academia and industry Preface by the section editors (2003)

Bengt Jonsson, Konstantinos Sagonas

Abstract. ASTEC (Advanced Software TEChnology) is a competence center for industrially relevant research on software technology, centered in Uppsala, Stockholm, and Väster˚as. It is organized as a...

Insights to Angluin’s learning (2003)

Therese Berg, Bengt Jonsson, Martin Leucker, Mayank Saksena

Angluin presented an algorithm for learning a deterministic finite-state automaton in [Ang87]. It continuously constructs an approximation of the automaton in question by querying a so-called teacher...

Processor pipelines and their properties for static WCET analysis (2002)

Jakob Engblom, Bengt Jonsson

www.it.uu.se Abstract. When developing real-time systems, the worst-case execution time (WCET) is a commonly used measure for predicting and analyzing program and system timing behavior. Such...

Model Checking of Systems with Many Identical Timed Processes (2002)

Parosh Aziz Abdulla, Bengt Jonsson, 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...

Probabilistic extensions of process algebras (2001)

Bengt Jonsson, Kim G Larsen, Wang Yi

In this chapter, we adopt Probabilistic Transition Systems as a basic model for probabilistic processes, in which probabilistic and nondeterministic choices are independent concepts. The model is...

An Execution Semantics for MSC-2000 (2001)

Bengt Jonsson, Gerardo Padilla

Abstract. Message Sequence Charts (MSCs) is a visual notation for expressing requirements on communicating systems. Their expressive power has traditionally been somewhat limited, and additional...

A Tool for Extracting the Process Structure of Erlang Applications. Erlang User Conference (2001)

Jan Nyström, Bengt Jonsson

Erlang is a concurrent functional language, especially tailored for distributed and fault-tolerant software. Its strength has been demonstrated by several successful commercial applications. An...

Algorithmic Analysis of Programs with Well Quasi-Ordered Domains (2000)

Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, Yih-kuen Tsay

Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. This paper is concerned with identifying general...

Proving refinement using transduction (1999)

Bengt Jonsson, Amir Pnueli, Camilla Rump

Summary. When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given at different levels of abstraction. Suggested verification...

On the existence of network invariants for verifying parameterized systems (1999)

Parosh Aziz Abdulla, Bengt Jonsson

Over the last decade, finite-state verification methods have been developed to an impressive tool for analysis of complex programs, such as protocols and hardware circuits. Partial-order reduction...

Handling global conditions in parametrized system verification (1999)

Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson

We consider symbolic verification for a class of parametrized systems, where a system consists of a linear array of processes, and where an action of a process may in general be guarded by both local...

Handling Global Conditions in Parameterized System Verification (1999)

Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson

We consider symbolic verification for a class of parameterized systems, where a system consists of a linear array of processes, and where an action of a process may in general be guarded by both...

Towards Deductive Synthesis of Dataflow Networks, (1998)

Jonsson, Bengt, Manna, Zohar, Waldinger, Richard

The authors present a method for deductive synthesis of deterministic dataflow networks. A network is specified by a relation between sequences of input values and sequences of output values. From...

Partial Order Reductions for Timed Systems (1998)

Bengtsson, Johan, Jonsson, Bengt, Lilius, Johan, Yi, Wang

http://www.tucs.fi/Publications/proceedings/pBeJoLiYi98a.php

Partial order reductions for timed systems (1998)

Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi

Abstract. In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit clock...

On-the-fly analysis of systems with unbounded, lossy fifo channels (1998)

Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson

Abstract. We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel...

Partial Order Reductions for Timed Systems (1998)

Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi

. In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit clock...

Partial Order Reductions for Timed Systems (1998)

Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi

. In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit...

On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels (1998)

Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson

. We consider symbolic on-the-fly verification methods for systems of finitestate machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel...

Ensuring Completeness of Symbolic Verification Methods for Infinite-State Systems (1998)

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...

Verifying Networks of Timed Processes (1998)

Parosh Aziz Abdulla, Bengt Jonsson, 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...

Verifying Networks of Timed Processes (1998)

Parosh Aziz Abdulla, Bengt Jonsson, 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...

Partial Order Reductions for Timed Systems (1998)

Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi

Partial-order reduction has been successfully applied to state-space exploration for untimed systems, often yielding substantial reductions in the usage of time and memory. However, for timed systems...

A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract) (1998)

Parosh Aziz Abdulla, Bengt Jonsson, Mats Kindahl, Doron Peled

The purpose of partial-order verification techniques is to avoid exploring several interleavings of independent transitions. The purpose of symbolic verification techniques is to perform basic...

Verifying Programs with Unreliable Channels (1996)

Parosh 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...

Verifying Programs with Unreliable Channels (1996)

Parosh Abdulla, Bengt Jonsson

The research on algorithmic verification methods for concurrent and parallel systems has mostly focussed on finite-state systems, with applications in e.g. communication protocols and hardware...

A Formalization of Service Independent Building Blocks (1996)

Jan Nyström, Bengt Jonsson

The objective of this paper is to present an effort to formalize the Service independent building blocks (SIBs) standardized by the ITU-T. The SIBs as an abstraction, but also as concrete building...

General Decidability Theorems for Infinite-State Systems (1996)

Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, Yih-Kuen Tsay

) Parosh Aziz Abdulla Uppsala University K¯arlis Cer¯ans University of Latvia Bengt Jonsson Uppsala University Yih-Kuen Tsay National Taiwan University Abstract Over the last few years there has...

Creation of Dependent Features (1996)

Johan Blom, Roland Bol, Bengt Jonsson, Jan Nyström

systems. It also occurs in operating systems of computers, car design, and the design of virtually all other large systems. But currently we concentrate on feature interactions in telecommunication,...

Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms (1995)

Bengt Jonsson, Lars Kempe

. We consider the problem of verifying correctness properties of a class of programs with states that are sets of ground atoms. Such programs can model specifications of telephone services, in which...

Compositional Testing Preorders for Probabilistic Processes (1995)

Bengt Jonsson, Wang Yi

Transition systems are well-established as a semantic model for distributed systems. There are widely accepted preorders that serve as criteria for refinement of a more abstract transition system to...

Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms (1995)

Bengt Jonsson, Lars Kempe

. We consider the problem of verifying correctness properties of a class of programs with states that are sets of ground atoms. Such programs can model specifications of telephone services, in which...

Testing and Refinement for Nondeterministic and Probabilistic Processes (1994)

Bengt Jonsson, Chris Ho-stuart, Wang Yi

. Transition systems are a basic semantic model for formal description, specification, and analysis of concurrent and distributed systems. In order to describe and analyze aspects of reliability,...

Decidability of Timed Language-Inclusion for Networks of Real-Time Communicating Sequential Processes (1994)

Wang Yi, Bengt Jonsson

. An important verification problem for concurrent systems in general is that of establishing whether one system is a correct implementation, or refinement, of another system. For untimed systems,...

A Logic for Reasoning about Time and Reliability (1994)

Hans Hansson, Bengt Jonsson

We present a logic for stating properties such as, "after a request for service there is at least a 98% probability that the service will be carried out within 2 seconds". The logic extends...

Undecidable Verification Problems for Programs with Unreliable Channels (1994)

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...

Proving Refinement Using Transduction (1994)

Bengt Jonsson, Amir Pnueli, Camilla Rump

When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given at different levels of abstraction. Suggested verification techniques in...

Undecidable Verification Problems for Programs with Unreliable Channels (1994)

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...

On Unifying Assumption--Commitment Style Proof Rules for Concurrency (1994)

Bengt Jonsson, Joachim Parrow (eds, Qiwen Xu, Antonio Cau

. Assumption--Commitment paradigms for specification and verification of concurrent programs have been proposed in the past. We show that two typical parallel composition rules for shared variable...

Indeterminate Concurrent Constraint Programming: A Fixpoint Semantics for Non-Terminating Computations (1994)

Sven-Olof Nyström, Bengt Jonsson

This paper presents a semantics for non-deterministic concurrent constraint programming languages. The semantics address the issues of giving an adequate treatment of non-terminating computations, in...

Using Temporal Logic for Modular Specification of Telephone Services (1994)

Johan Blom, Bengt Jonsson, Lars Kempe

. We outline a methodology for the modular specification of telephone services within first-order linear-time temporal logic. Typically, the services offered by a telephone system consist of a basic...

Verifying Programs with Unreliable Channels (1993)

Parosh 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...

On the complexity of equation solving in process algebra (1991)

Jonsson, Bengt, Guldstrand Larsen, Kim

The problem of designing a system which in a given environment C should satisfy a given specification S can be formulated as "find a system P such that C(P) satisfies the specifacation S". In process...

A hierarchy of compositional models of I/O.Automata (1991)

Jonsson, Bengt

A semantic model of computer systems is compositional if it adequately represents the behavior of the modeled systems in a context of other systems. A compositional model is thus a good basis for...

Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs (1991)

Bengt Jonsson, Joachim Parrow

Traditionally, many automatic program verification techniques are applicable only to finite-state programs. In this paper we extend some of these techniques to a class of infinite-state programs...

A logic for reasoning about time and reability (1990)

Hansson, Hans, Jonsson, Bengt

We present a logic for stating properties such as, "after a request for service there is at least a 98\045 probability that the service will be carried out within 2 seconds". The logic extends the...

A Fully Abstract Trace Model for Dataflow and Asynchronous Networks (1990)

Jonsson, Bengt

A dataflow network consists of nodes that communicate over perfect unbounded FIFO channels. For dataflow networks containing only deterministic nodes, a simple and elegant semantic model has been...

Compositional specification and verification of distributed systems (1990)

Jonsson, Bengt

We present a method for specification and verification of distributed systems that communicate via asynchronous message-passing. The method handles both safety and liveness properties. It is...

Specification and validation of a simple overtaking protocol using LOTOS (1990)

Ernberg, Patrik, Fredlund, Lars-åke, Jonsson, Bengt

We present a specification of a simple Overtaking protocol for vehicles using the Formal Description Technique LOTOS. A detailed description of the design process leading to this specification is...

Deciding bisimulation equivalences for a class of non-finite-state programs (1989)

Jonsson, Bengt, Parrow, Joachim

Traditionally, many automatic program verification techniques are applicable only to finite-state programs. In this paper we show how to extend some verification techniques to infinite-state programs...

A fully abstract trace model for dataflow networks (1988)

Jonsson, Bengt

A dataflow network consists of nodes that communicate over perfect FIFO channels. For dataflow networks containing only deterministic nodes, a simple and elegant semantic model has been presented by...

Effect of Changes in Ventricular Rate on Cardiac Output and Central Pressures at Rest and During Exercise in Patients with Artificial Pacemakers (1967)

Bevegård, Sture, Jonsson, Bengt, Karlöf, Ingvar, Lagergren, Hans, Sowton, Edgar

Authors' SynopsisThe stroke volume and central pressures were measured at rest and during exercise in 22 patients with heart block, aged between 14 and 78 years. The immediate and later effects of...

International comparisons of health expenditure: Theory, data and econometric analysis

Gerdtham, Ulf-G., Jonsson, Bengt, A. J. Culyer, J. P. Newhouse

Comparisons of aggregate health expenditure across different countries have become popular over the last three decades as they permit a systematic investigation of the impact of different...

The Economic Cost of Multiple Sclerosis in Sweden in 1994

Freddie Henriksson, Bengt Jonsson

This paper investigates the economic burden of multiple sclerosis (MS) in Sweden in 1994. The cost structure was compared with costs from a similar study from 1991 and 3 studies from the UK. The...

Advantages of Using the Net-Benefit Approach for Analysing Uncertainty in Economic Evaluation Studies

Niklas Zethraeus, Magnus Johannesson, Bengt Jonsson, Mickael Lothgren, Magnus Tambour

No consensus has yet been reached on how to analyse uncertainty in economic evaluation studies where individual patient data are available for costs and health effects. This paper summarises the...

Cost Effectiveness of Alendronate (Fosamax(R)) for the Treatment of Osteoporosis and Prevention of Fractures

Olof Johnell, Bengt Jonsson, Linus Jonsson, Dennis Black

Background: The Fracture Intervention Trial (FIT) demonstrated that the bisphosphonate alendronate reduces the risk of hip, spine and wrist fracture in osteoporotic women by approximately one half....

Costs and Cost Effectiveness of Low Molecular Weight Heparins and Platelet Glycoprotein IIb/IIIa Inhibitors: In the Management of Acute Coronary Syndromes

Nick Bosanquet, Bengt Jonsson

The most well established antithrombotic treatment for acute coronary syndromes (ACS) is unfractionated heparin (UFH) plus aspirin, but such treatment may not prevent arterial thrombotic events. Low...

Cost Effectiveness of Raloxifene in the Treatment of Osteoporosis in Sweden: An Economic Evaluation Based on the MORE Study

Fredrik Borgstrom, Olof Johnell, John A. Kanis, Anders Oden, David Sykes, Bengt Jonsson

Background: The Multiple Outcomes of Raloxifene Evaluation (MORE) study showed that treatment with raloxifene reduces the risk of vertebral fracture and breast cancer in postmenopausal women with...

Cost Effectiveness of Bisoprolol in the Treatment of Chronic Congestive Heart Failure in Sweden: Analysis Using Data from the Cardiac Insufficiency Bisoprolol Study II Trial

Mattias Ekman, Niklas Zethraeus, Bengt Jonsson

Objective: To investigate the cost effectiveness of adding the beta-blocker bisoprolol to standard treatment in patients with congestive heart failure (CHF). Design and setting: A cost-effectiveness...

Cost-Effectiveness Analysis of Exemestane Compared with Megestrol in Advanced Breast Cancer: A Model for Europe and Australia

Peter Lindgren, Bengt Jonsson, Alberto Redaelli, Davide Radice

Objective: To investigate the cost effectiveness of exemestane compared to megestrol in post-menopausal women after tamoxifen failure. Design and setting: A modelling study from the third-party payer...

Costs of Mini Mental State Examination-Related Cognitive Impairment

Linus Jonsson, Peter Lindgren, Anders Wimo, Bengt Jonsson, Bengt Winblad

Objective: To investigate the relationship between cognitive impairment, measured with the Mini Mental State Examination (MMSE), and the cost of care. Design: The study uses data from the Kungsholmen...

Transitive Closures of Regular Relations for Verifying Infinite-State Systems

Bengt Jonsson, Marcus Nilsson

. We consider a model for representing infinite-state and parameterized systems, in which states are represented as strings over a finite alphabet. Actions are transformations on strings, in which...

The Lifetime Cost Effectiveness of Amlodipine-Based Therapy Plus Atorvastatin Compared with Atenolol Plus Atorvastatin, Amlodipine-Based Therapy Alone and Atenolol-Based Therapy Alone: Results from ASCOT1

Peter Lindgren, Martin Buxton, Thomas Kahan, Neil R. Poulter, Bjrn Dahlf, Peter S. Sever, ...

Background: ASCOT (Anglo-Scandinavian Cardiac Outcomes Trial) showed in hypertensive patients that blood pressure-lowering treatment with an amlodipine-based regimen reduces events compared with an...