Publications by Bengt Jonsson

sorted by topics: Automated Verification | Specification and Refinement | Probabilistic and Real-Time Aspects | Semantics

This page is under construction!!!

Papers on Automated Verification

• Ensuring Completeness of Symbolic Verification Methods for Infinite-State Systems..
  Parosh Aziz Abdulla, Bengt Jonsson.
  Submitted Manuscript, 1997. abstract | full version: postscript
• Verifying Networks of Timed Processes.
  Parosh Aziz Abdulla, Bengt Jonsson.
  Submitted Manuscript, 1997. abstract | full version: postscript
• General decidability theorems for infinite-state systems.
  Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Tsay Yih-Kuen.
  In Proc. 11th IEEE Int. Symp. on Logic in Computer Science, pages 313--321, 1996. abstract
• Undecidable verification problems for programs with unreliable channels.
  Parosh Aziz Abdulla and Bengt Jonsson.
  Information and Computation, 130(1):71-90, October 10, 1996.
  abstract
  In Abiteboul and Shamir, editors, Proc. ICALP '94, volume 820 of Lecture Notes in Computer Science, pages 316--327. Springer Verlag, 1994.
• Verifying programs with unreliable channels.
  Parosh Aziz Abdulla and Bengt Jonsson.
  Information and Computation, 127(2):91-101, June 15, 1996.
  abstract
  In Proc. 8th IEEE Int. Symp. on Logic in Computer Science, pages 160--170, 1993.
• Verifying safety properties of a class of infinite-state distributed algorithms.
  Bengt Jonsson and Lars Kempe.
  In Proc. 7th Int. Conf. on Computer Aided Verification, volume 939 of Lecture Notes in Computer Science, pages 42--53. Springer Verlag, 1995.
  abstract | full version: postscript
• Validating simulations between large nondeterministic specifications.
  R. Civalero, B. Jonsson, and J. Nilsson.
  In Proc. FORTE '93. North-Holland, 1993.
• Deciding bisimulation equivalences for a class of Non-Finite-State programs.
  Bengt Jonsson and Joachim Parrow.
  Information and Computation, 107(2):272-302, December 1993.
  In Monien and Cori, editors, Proc. $6$th Symposium on Theoretical Aspects of Computer Science, volume 349 of Lecture Notes in Computer Science, pages 421--433. Springer Verlag, 1989.
• On the complexity of equation solving in process algebra.
  B. Jonsson and K. Larsen.
  In Abramsky and Maibaum, editors, Proc. Coll. on Trees and Algebra in Programming, volume 493 of Lecture Notes in Computer Science, pages 381--396. Springer Verlag, 1991. Extended Version as SICS Research Report 91:05.
• Implementing a model checking algorithm by combining existing automated tools.
  B. Jonsson, A. Khan, and J. Parrow.
  In Sifakis, editor, Proc. Workshop on Computer Aided Verification, volume 407 of Lecture Notes in Computer Science. Springer Verlag, 1990.

Papers on Specification and Refinement

• Assumption/guarantee specifications in linear-time temporal logic.
  Bengt Jonsson and Yih-Kuen Tsay.
  Theoretical Computer Science, 167(1-2):47-72, 30 October 1996
  In Mosses, Nielsen, and Schwartzbach, editors, TAPSOFT '95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 262--276. Springer Verlag, 1995.
• Proving refinement using transduction.
  B. Jonsson, A. Pnueli, and C. Rump.
  Technical Report DoCS 94/54, Dept. of Computer Systems, Uppsala University, Sweden, 1994. A simultaneous technical report of Lyngby, Uppsala, and Weizmann.
  full version: postscript
• The Dagstuhl case study -- architecture oriented temporal logic specification.
  J. Blom and B. Jonsson.
  Contribution to Case Study on Specification of an RPC Memory Module, to appear in Lecture Notes in Computer Science, Springer Verlag, June 1996.
• Using temporal logic for modular specification of telephone services.
  J. Blom, B. Jonsson, and L. Kempe.
  In L.G. Bouma and H. Velthuijsen, editors, Feature Interactions in Telecommunications Systems. IOS Press, Amsterdam, Netherlands, May 1994.
• Compositional specification and verification of distributed systems.
  B. Jonsson.
  ACM Trans. on Programming Languages and Systems, 16(2):259--303, 1994.
  preliminary version as
  Modular verification of asynchronous networks.
  B. Jonsson.
  In Proc. 6th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 152--166, Vancouver, Canada, 1987.
• Refining interfaces of communicating systems. E. Brinksma, B. Jonsson, and F. Orava.
  In Abramsky and Maibaum, editors, Proc. Coll. on Combining Paradigms for Software Development, volume 494 of Lecture Notes in Computer Science, pages 297--312. Springer Verlag, 1991.
• Simulations between specifications of distributed systems.
  B. Jonsson.
  In Proc. CONCUR '91, Theories of Concurrency: Unification and Extension, number 527 in Lecture Notes in Computer Science, Amsterdam, Holland, 1991. Springer Verlag.
• Specification and validation of a simple overtaking protocol using LOTOS.
  P. Ernberg, L.-å. Fredlund, and B. Jonsson.
  In G. Rose, editor, Proc. FORTE '91, Sydney, Australia, Nov. 1991. North-Holland.
• On decomposing and refining specifications of distributed systems.
  B. Jonsson.
  In de Bakker, de Roever, and Rozenberg, editors, Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 361--385. Springer Verlag, 1990.
• A model and proof system for asynchronous networks.
  B. Jonsson.
  In Proc. 4th ACM Symp. on Principles of Distributed Computing, pages 49--58, Minaki, Canada, 1985.

Papers on Probabilistic and Real-Time Aspects

• Compositional testing preorders for probabilistic processes.
  B. Jonsson and W. Yi.
  In Proc. 10th IEEE Int. Symp. on Logic in Computer Science, pages 431--441, 1995.
• Testing and refinement for nondeterministic and probabilistic processes.
  B. Jonsson, C. Ho-Stuart, and W. Yi.
  In Langmaack, de Roever, and Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 418--430. Springer Verlag, 1994.
• Decidability of timed language-inclusion for networks of real-time communicating sequential processes.
  Wang Yi and B. Jonsson.
  In Proc. 14th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 880 of Lecture Notes in G Computer Science. Springer Verlag, 1994.
• Specification and refinement of probabilistic processes.
  B. Jonsson and K. Larsen.
  In Proc. 6th IEEE Int. Symp. on Logic in Computer Science, Amsterdam, Holland, July 1991.
• A logic for reasoning about time and reliability.
  Hans Hansson and Bengt Jonsson.
  Formal Aspects of Computing 6(5):512-535, 1994.
  a preliminary version appeared as:
  A framework for reasoning about time and reliability.
  H. Hansson and B. Jonsson.
  In Proc. 10th IEEE Real -Time Systems Symposium, S:a Monica, Ca., 1989.

Papers on Semantics

• Indeterminate concurrent constraint programming: A fixpoint semantics for non-terminating computations.
  S.-O. Nyström and B. Jonsson.
  In International Logic Programming Symposium, Vancouver, British Columbia, Canada, Oct. 1993.
• Comparing two fully absttract dataflow models.
  B. Jonsson and J. Kok.
  In Proc. PARLE '89, volume 365 of Lecture Notes in Computer Science, pages 217--234. Springer Verlag, 1989.
• A fully abstract trace model for dataflow and asynchronous networks.
  B. Jonsson.
  Distributed Computing, 7:197--212, 1994.
  Preliminary version as
  A fully abstract trace model for dataflow networks.
  B. Jonsson.
  In Proc. 16th ACM Symp. on Principles of Programming Languages, pages 155--165, 1989.
• A hierarchy of compositional models of I/O-automata.
  B. Jonsson.
  In Rovan, editor, Proc. Mathematical Foundations of Computer Science, volume 452 of Lecture Notes in Computer Science, pages 347--354. Springer Verlag, 1990. Extended Version as SICS Research Report 91:04.