Helsinki University of Technology, Laboratory for Theoretical Computer Science

Formal Methods in Distributed Systems

A research project funded by the Academy of Finland (project number 47754)
Jan 1, 2000 - Dec 31, 2002

Project leader:
Prof. Leo Ojala (Jan 1, 2000 - Nov 30, 2000)
Prof. Ilkka Niemelä (Dec 1, 2000 - Dec 31, 2002)

Research Personnel: Tomi Janhunen, Tuomas Aura, Keijo Heljanko, Harri Haanpää, Tommi Junttila, Petteri Kaski, Timo Latvala, Marko Mäkelä, Teemu Tynjälä, Silja Mäki, Heikki Tauriainen, Rauni Pääkkönen, Harriet Beaver, Elina Parviainen

Summary: This project continues earlier research work on the analysis and design methods for parallel and distributed systems in the Laboratory for Theoretical Computer Science. The aim is to develop new analysis and verification methods for parallel and distributed systems based on partial order semantics, symmetries and data abstraction, methodology for designing and analyzing multi-agent systems and formal models for information security systems.

The project continues earlier research in the TCS laboratory on the analysis and design methods of parallel and distributed systems. The plan of the project divided research work into work packages WP1-WP5. Due to partiality of the funding granted by the Academy of Finland, the work package WP3 (Modeling and Verification of Safety Critical Systems) was moved to the Maria project (funded by industry and the National Technology Agency of Finland) in the beginning of the year 2000.

In the work-package WP1 (Model Checking), we have created and implemented an LTL model checker based on finite complete prefixes [11,12,47,48,13] and parallelised a prefix generation procedure [15,49]. Many of these results can be found in Keijo Heljanko's doctoral dissertation [39] that was accepted in April 2002. The research in WP1 has also produced methods for the automated testing of model checkers [5,35], for handling of fairness properties [3,23], for model checking of safety properties [19,20,22,23,24,42,55], for bounded model checking [1,14,16,17,50] and for stubborn set optimization [6,37]. A number of case studies have been conducted [4,27,28,36,43].

In WP2 (Symmetries and Data Abstraction in Verification), we have investigated the computational complexity of the sub-problems appearing in the symmetry reduction method when applied to place/transition nets [2,52]. In addition, we have developed new algorithms for comparing whether two states are equivalent under symmetries and for producing equivalent representatives for states [54,53]. Tommi Junttila's doctoral dissertation on the symmetry method containing main results of WP3 has been submitted for preliminary examination [40].

In WP4 (Agent-based Framework), a declarative language has been designed for the formal description of multi-agent systems by combining features from both rule-based languages and Petri nets in order to obtain a more expressive language [51]. We have implemented a prototype system [45] that enables automated execution of specifications in this language.

In WP5 (Formal Models for Information Security Systems), we have dealt with the use of certificates in network security protocols [10,25,26,46] as well as methods against denial of service attacks [7,8,9,18,21]. Many of the results of WP5 can be found in Tuomas Aura's doctoral dissertation [38] that was accepted in December 2000.

Modelling of quantum computation using Petri nets as the formal model has been investigated [29,30,31,32,33,44].

The research has been carried out in close cooperation with the projects 43963 (Constraint Programming Based on Default Rules) and 53695 (Applications of Rule-Based Constraint Programming) funded by the Academy of Finland. In particular, the rule-based constraint programming paradigm has been exploited in (i) developing efficient model checking techniques based on finite complete prefixes and bounded model checking, (ii) analysis of network security, and (iii) specification of multi-agent systems.

Keywords: Parallel and distributed systems, verification, agent-based computing, security

Degrees

Tuomas Aura, D.Sc. (Tech.), 2000 [38]
Supervisor: Prof. Ilkka Niemelä
Graduate School: HeCSE

Keijo Heljanko, D.Sc. (Tech.), 2002 [39]
Supervisor: Prof. Ilkka Niemelä
Graduate School: HeCSE

Petteri Kaski, Lic.Sc. (Tech.), 2002 [41]
Supervisor: Prof. Pekka Orponen
Graduate School: HeCSE

Timo Latvala, Lic.Sc. (Tech.) 2002 [42]
Supervisor: Prof. Nisse Husberg
Graduate School: HeCSE

Teemu Tynjälä, Lic.Sc. (Tech.), 2003 [43]
Supervisor: Prof. Nisse Husberg
Graduate School: HeCSE

Rauni Pääkkönen, M.Sc. (Tech.), 2001 [45]
Supervisor: Prof. Ilkka Niemelä

Software

Bibliography

Articles in international scientific journals with referee practice

1
Keijo Heljanko and Ilkka Niemelä, ``Bounded LTL Model Checking with Stable Models,'' Theory and Practice of Logic Programming. Accepted for publication.

2
Tommi Junttila, ``Computational Complexity of the Place/Transition-Net Symmetry Reduction Method,'' Journal of Universal Computer Science, Vol. 7, No. 4, 2001, pp. 307-326.

3
Timo Latvala and Keijo Heljanko, ``Coping with Strong Fairness,'' Fundamenta Informaticae (Annales Societatis Mathematicae Polonae, Series IV), Vol. 43, No. 1-4, 2000, pp. 175-193.

4
Leo Ojala, Nisse Husberg, and Teemu Tynjälä, ``Modelling and analysing a distributed dynamic channel allocation algorithm for mobile computing using high-level net methods,'' International Journal on Software Tools for Technology Transfer, Vol. 3, No. 4, 2001, pp. 382-393. http://link.springer.de/link/service/journals/10009/bibs/1003004/10030382.htm

5
Heikki Tauriainen and Keijo Heljanko, ``Testing LTL Formula Translation into Büchi Automata,'' International Journal on Software Tools for Technology Transfer, Vol. 4, No. 1, 2002, pp. 57-70.
http://link.springer.de/link/service/journals/10009/bibs/2004001/20040057.htm

6
Kimmo Varpaaniemi, ``Towards Ambitious Approximation Algorithms in Stubborn Set Optimization,'' Fundamenta Informaticae (Annales Societatis Mathematicae Polonae, Series IV), Vol. 54, No. 2-3, 2003, pp. 279-294.

Articles in international scientific conference proceedings with referee practice

7
Tuomas Aura, ``DOS-Resistant Authentication with Client Puzzles (Transcript of Discussion),'' in B. Christianson, B. Crispo, J.A. Malcolm, and M. Roe (Eds.), Security Protocols, 8th International Workshop, Cambridge, UK, April 3-5, 2000, Revised Papers, Lecture Notes in Computer Science, Vol. 2133, Springer-Verlag, Berlin, Germany, 2001, pp. 178-181. http://link.springer.de/link/service/series/0558/bibs/2133/21330178.htm

8
Tuomas Aura, Matt Bishop, and Dean Sniegowski, ``Analyzing single-server network inhibition,'' in Proceedings of the 2000 IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos CA, USA, 2000, pp. 108-117.
http://ieeexplore.ieee.org/xpl/tocresult.jsp?isNumber=18612&page=0

9
Tuomas Aura, Pekka Nikander, and Jussipekka Leiwo, ``DOS-Resistant Authentication with Client Puzzles,'' in B. Christianson, B. Crispo, J.A. Malcolm, and M. Roe (Eds.), Security Protocols, 8th International Workshop, Cambridge, UK, April 3-5, 2000, Revised Papers, Lecture Notes in Computer Science, Vol. 2133, Springer-Verlag, Berlin, Germany, 2001, pp. 170-177.
http://link.springer.de/link/service/series/0558/bibs/2133/21330170.htm

10
Tuomas Aura and Silja Mäki, ``Towards a Survivable Security Architecture for Ad Hoc Networks,'' in B. Christianson, B. Crispo, J.A. Malcolm, and M. Roe (Eds.), Security Protocols, 9th International Workshop, Cambridge, UK, April 25-27, 2001, Revised Papers, Lecture Notes in Computer Science, Vol. 2467, Springer-Verlag, Berlin, Germany, 2002, pp. 63-73. http://link.springer.de/link/service/series/0558/bibs/2467/24670063.htm

11
Javier Esparza and Keijo Heljanko, ``A New Unfolding Approach to LTL Model Checking,'' in U. Montanari, J.D.P. Rolim, and E. Welzl (Eds.), Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 1853, Springer-Verlag, Berlin, Germany, 2000, pp. 475-486. http://link.springer.de/link/service/series/0558/bibs/1853/18530475.htm

12
Javier Esparza and Keijo Heljanko, ``Implementing LTL Model Checking with Net Unfoldings,'' in M.B. Dwyer (Ed.), Model Checking Software, 8th International SPIN Workshop, Lecture Notes in Computer Science, Vol. 2057, Springer-Verlag, Berlin, Germany, 2001, pp. 37-56. http://link.springer.de/link/service/series/0558/bibs/2057/20570037.htm

13
Keijo Heljanko, ``Model Checking with Finite Complete Prefixes is PSPACE-Complete,'' in C. Palamidessi (Ed.), CONCUR 2000 -- Concurrency Theory, Lecture Notes in Computer Science, Vol. 1877, Springer-Verlag, Berlin, Germany, 2000, pp. 108-122.
http://link.springer.de/link/service/series/0558/bibs/1877/18770108.htm

14
Keijo Heljanko, ``Bounded Reachability Checking with Process Semantics,'' in K.G. Larsen and M. Nielsen (Eds.), CONCUR 2001 -- Concurrency Theory, Lecture Notes in Computer Science, Vol. 2154, Springer-Verlag, Berlin, Germany, 2001, pp. 218-232. http://link.springer.de/link/service/series/0558/bibs/2154/21540218.htm

15
Keijo Heljanko, Victor Khomenko, and Maciej Koutny, ``Parallelisation of the Petri Net Unfolding Algorithm,'' in J.-P. Katoen and P. Stevens (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 2280, Springer-Verlag, Berlin, Germany, 2002, pp. 371-385. http://link.springer.de/link/service/series/0558/bibs/2280/22800371.htm

16
Keijo Heljanko and Ilkka Niemelä, ``Answer Set Programming and Bounded Model Checking,'' in Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning, AAAI Press, 2001, pp. 90-96. http://www.tcs.hut.fi/~ini/papers/HelNie-ASP2001.ps.gz

17
Keijo Heljanko and Ilkka Niemelä, ``Bounded LTL Model Checking with Stable Models,'' in T. Eiter, W. Faber, and M. Truszczynski (Eds.), Logic Programming and Nonmonotonic Reasoning, Lecture Notes in Artificial Intelligence, Vol. 2173, Springer-Verlag, Berlin, Germany, 2001, pp. 200-212.
http://link.springer.de/link/service/series/0558/bibs/2173/21730200.htm

18
John R. Hughes, Tuomas Aura, and Matt Bishop, ``Using conservation of flow as a security mechanism in network protocols,'' in Proceedings of the 2000 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Los Alamitos CA, USA, 2000, pp. 132-141. http://ieeexplore.ieee.org/xpl/tocresult.jsp?isNumber=18435&page=0

19
Jukka Järvenpää and Marko Mäkelä, ``Towards Automated Checking of Component-Oriented Enterprise Applications,'' in D. Moldt (Ed.), Second Workshop on Modelling of Objects, Components and Agents, Aarhus, Denmark, August 26-27, 2002, University of Aarhus, Department of Computer Science, Report DAIMI PB-561, 2002, pp. 67-85. http://www.daimi.au.dk/CPnets/workshop02/moca/papers/

20
Timo Latvala, ``Efficient Model Checking of Safety Properties,'' in T. Ball and S.K. Rajamani (Eds.), Model Checking Software, 10th International SPIN Workshop, Portland, OR, USA, May 9-10, 2003, Proceedings, Lecture Notes in Computer Science, Vol. 2648, Springer-Verlag, Berlin, Germany, 2003, pp. 74-88.
http://link.springer.de/link/service/series/0558/bibs/2648/26480074.htm

21
Jussipekka Leiwo, Tuomas Aura, and Pekka Nikander, ``Towards network denial of service resistant protocols,'' in S. Qing and J.H.P. Eloff (Eds.), Information Security for Global Information Infrastructures, IFIP Series, Vol. 175, Kluwer Academic Publishers, Boston, MA, USA, 2000, pp. 301-310.

22
Marko Mäkelä, ``Efficiently Verifying Safety Properties with Idle Office Computers,'' in C. Lakos, R. Esser, L.M. Kristensen, and J. Billington (Eds.), Formal Methods in Software Engineering and Defence Systems 2002, Proceedings of the Workshops on Software Engineering and Formal Methods and Formal Methods Applied to Defence Systems, Conferences in Research and Practice in Information Technology, Vol. 12, Australian Computer Society Inc., Sydney, Australia, 2002, pp. 11-16. http://CRPIT.com/Vol12.html

23
Marko Mäkelä, ``Maria: Modular Reachability Analyser for Algebraic System Nets,'' in J. Esparza and C. Lakos (Eds.), Application and Theory of Petri Nets 2002, Lecture Notes in Computer Science, Vol. 2360, Springer-Verlag, Berlin, Germany, 2002, pp. 434-444. http://link.springer.de/link/service/series/0558/bibs/2360/23600434.htm

24
Marko Mäkelä, ``Model Checking Safety Properties in Modular High-Level Nets,'' in W.M.P. van der Aalst and E. Best (Eds.), Application and Theory of Petri Nets 2003, 24th International Conference, ICATPN 2003, Eindhoven, The Netherlands, June 23-27, 2003, Proceedings, Lecture Notes in Computer Science, Vol. 2679, Springer-Verlag, Berlin, Germany, 2003, pp. 201-220.
http://link.springer.de/link/service/series/0558/bibs/2679/26790201.htm

25
Silja Mäki, ``Towards a Survivable Security Architecture for Ad Hoc Networks (Transcript of Discussion),'' in B. Christianson, B. Crispo, J.A. Malcolm, and M. Roe (Eds.), Security Protocols, 9th International Workshop, Cambridge, UK, April 25-27, 2001, Revised Papers, Lecture Notes in Computer Science, Vol. 2467, Springer-Verlag, Berlin, Germany, 2002, pp. 74-79.
http://link.springer.de/link/service/series/0558/bibs/2467/24670074.htm

26
Silja Mäki, Tuomas Aura, and Maarit Hietalahti, ``Robust Membership Management for Ad-hoc Groups,'' in U. Erlingsson (Ed.), NordSec 2000 -- Proceedings of the Fifth Nordic Workshop on Secure IT Systems, Reykjavik University, Iceland, 2000, pp. 151-168. http://www.tcs.hut.fi/old/papers/aura/maki-aura-hietalahti-nordsec00-abstract.html

27
Leo Ojala, Nisse Husberg, and Teemu Tynjälä, ``Modelling and Analysing a Distributed Dynamic Channel Allocation Algorithm for Mobile Computing Using High-Level Net Methods,'' in K. Jensen (Ed.), Practical Use of High-Level Petri Nets, DAIMI PB-547, University of Aarhus, Denmark, 2000, pp. 73-90.
http://www.daimi.au.dk/pn2000/proceedings/pn2000_hlpnworkshop.pdf

28
Leo Ojala, Nisse Husberg, and Teemu Tynjälä, ``Modelling a Distributed Wireless Channel Allocation Algorithm for Cellular Systems with Mobile Base Stations Using Predicate/Transition Nets,'' in J. Lee, M. Juric, A. Bruzzone, D. Klovshy, and M. Fujita (Eds.), SCI2000 / ISAS2000 (The 4th World Multiconference on Systemics, Cybernetics and Informatics / The 6th International Conference on Information Systems, Analysis and Synthesis), Orlando, FL, USA, July 23-26, Proceedings, Vol. VIII (Computer Science and Engineering: Part II), IIIS (International Institute of Informatics and Systemics), Orlando, FL, USA, 2000, pp. 678-683.

29
Leo Ojala, Elina Parviainen, Olli-Matti Penttinen, Harriet Beaver, and Teemu Tynjälä, ``Modeling Feynman's Quantum Computer using Stochastic High Level Petri Nets,'' in Proceedings of the 2001 IEEE International Conference on Systems, Man and Cybernetics, Tucson, AZ, USA, October 7-9, 2001, Vol. 4, IEEE, 2001, pp. 2735-2741. http://ieeexplore.ieee.org/xpl/tocresult.jsp?isNumber=20944&page=7

30
Leo Ojala, Elina Parviainen, Olli-Matti Penttinen, and Juha Reunanen, ``Feynman's Quantum Computer Modeled Using Petri Nets: A Case Study,'' in N.C. Callaos, T. Leng, and B. Sanchez (Eds.), SCI2002 / ISAS2002 (The 6th World Multiconference on Systemics, Cybernetics and Informatics / The 8th International Conference on Information Systems, Analysis and Synthesis), Orlando, FL, USA, July 14-18, 2002, Proceedings, Vol. V (Computer Science I), IIIS (International Institute of Informatics and Systemics), Orlando, FL, USA, 2002.

31
Leo Ojala, Elina Parviainen, Olli-Matti Penttinen, Teemu Tynjälä, and Harriet Beaver, ``Modeling Feynman's Serial Quantum Computer Using Stochastic Petri Nets,'' in H.R. Arabnia(Ed.), Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA'02, Las Vegas, NV, USA, June 24-27, 2002, Vol. III, CSREA (Computer Science, Research, Education, and Applications) Press, Athens, GA, USA, 2002, pp. 1223-1229.

32
Leo Ojala, Teemu Tynjälä, and Harriet Beaver, ``Modeling Serial Quantum Processors Using Petri Nets,'' in N.C. Callaos, F.G. Tinetti, J.M. Champarnaud, and J.K. Lee (Eds.), SCI2001 / ISAS2001 (The 5th World Multiconference on Systemics, Cybernetics and Informatics / The 7th International Conference on Information Systems, Analysis and Synthesis), Orlando, FL, USA, July 22-25, 2001, Proceedings, Vol. XIV (Computer Science and Engineering: Part II), IIIS (International Institute of Informatics and Systemics), Orland, FL, USA, 2001, pp. 463-468.

33
Elina Parviainen, ``Reducing Size of Quantum Gate Matrices Using Pr/T-Nets,'' in Proceedings of the 2002 IEEE International Conference on Systems, Man and Cybernetics, Hammamet, Tunisia, October 6-9, 2002, Vol. 2, IEEE, 2002, pp. 634-639. http://ieeexplore.ieee.org/xpl/tocresult.jsp?isNumber=26297&page=7

34
Tuomo Pyhälä and Keijo Heljanko, ``Specification Coverage Aided Test Selection,'' in Proceedings og the 3rd International Conference on Application of Concurrency to System Design (ACSD'2003), Guimarães, Portugal, June 18-20, 2003. Accepted for publication.

35
Heikki Tauriainen and Keijo Heljanko, ``Testing SPIN's LTL Formula Conversion into Büchi Automata with Randomly Generated Input,'' in K. Havelund, J. Penix, and W. Visser (Eds.), SPIN Model Checking and Software Verification, Lecture Notes in Computer Science, Vol. 1885, Springer-Verlag, Berlin, Germany, 2000, pp. 54-72.

36
Teemu Tynjälä, Sari Leppänen, and Vesa Luukkala, ``Verifying Reliable Data Transmission over UMTS Radio Interface with High Level Petri Nets,'' in D.A. Peled and M.Y. Vardi (Eds.), Formal Techniques for Networked and Distributed Systems -- FORTE 2002, Lecture Notes in Computer Science, Vol. 2529, Springer-Verlag, Berlin, Germany, 2002, pp. 178-193. http://link.springer.de/link/service/series/0558/bibs/2529/25290178.htm

37
Kimmo Varpaaniemi, ``Towards Ambitious Approximation Algorithms in Stubborn Set Optimization,'' in H.-D. Burkhard, L. Czaja, G. Lindemann, A. Skowron, and P.H. Starke (Eds.), Workshop: Concurrency, Specification and Programming, CS&P'2002, Berlin, October 7-9, Vol. 2, Humboldt University Berlin, Department of Computer Science, Technical Report 161, Berlin, Germany, 2002, pp. 370-379.
http://www.tcs.hut.fi/Publications/info/kva.Vrp02c.shtml

Doctoral dissertations

38
Tuomas Aura, Authorization and Availability -- Aspects of Open Network Security, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A64. Espoo, November 2000, 42 pp. Supervised in Laboratory for Theoretical Computer Science by Professor Ilkka Niemelä. Department of Computer Science and Engineering conferred the degree of D.Sc. (Tech.) on December 15, 2000.
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A64.shtml

39
Keijo Heljanko, Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A71. Espoo, February 2002, 55+112 pp. Supervised in Laboratory for Theoretical Computer Science by Professor Ilkka Niemelä. Department of Computer Science and Engineering conferred the degree of D.Sc. (Tech.) on April 22, 2002.
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A71.shtml

40
Tommi Junttila, On the Symmetry Reduction Method for Petri Nets and Related Formalisms. Submitted for preliminary examination.

Licentiate's theses

41
Petteri Kaski, A Census of Steiner Triple Systems and Some Related Combinatorial Objects, December 2002, 83 pp. Supervised in Laboratory for Theoretical Computer Science by Professor Pekka Orponen. Department of Computer Science and Engineering conferred the degree of Lic.Sc. (Tech.) on December 19, 2002.

42
Timo Latvala, On Model Checking Safety Properties, December 2002, 64 pp. Supervised in Laboratory for Theoretical Computer Science by Professor (pro tem) Nisse Husberg. Department of Computer Science and Engineering conferred the degree of Lic.Sc. (Tech.) on December 19, 2002. Published as [55].

43
Teemu Tynjälä, Combining abstractions and reachability analysis: A case study of the RLC protocol, March 2003, 61 pp. Supervised in Laboratory for Theoretical Computer Science by Professor (pro tem) Nisse Husberg. Department of Computer Science and Engineering conferred the degree of Lic.Sc. (Tech.) on March 17, 2003.

Master's theses

44
Elina Parviainen. Modeling the Operation of Margolus Quantum Cellular Automaton Using High-Level Petri Nets, June 2002, 64 pp. Supervised in Laboratory for Theoretical Computer Science by Professor Ilkka Niemelä. Department of Computer Science and Engineering accepted the thesis on June 10, 2002.
http://www.tcs.hut.fi/Publications/info/bibdb.ParviainenMsc.shtml

45
Rauni Pääkkönen, Implementing a formal agent description language, December 2001, 62 pp. Supervised in Laboratory for Theoretical Computer Science by Professor Ilkka Niemelä. Department of Computer Science and Engineering conferred the degree of M.Sc. (Tech.) on December 17, 2001.

Other scientific publications

46
Tuomas Aura and Carl Ellison, Privacy and Accountability in Certificate Systems, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A61, Espoo, April 2000, 17 pp.
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A61.shtml

47
Javier Esparza and Keijo Heljanko, A New Unfolding Approach to LTL Model Checking, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A60, Espoo, April 2000, 32 pp.
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A60.shtml

48
Javier Esparza and Keijo Heljanko, Implementing LTL Model Checking with Net Unfoldings, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A68, Espoo, March 2001, 29 pp.
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A68.shtml

49
Keijo Heljanko, Victor Khomenko, and Maciej Koutny, Parallelisation of the Petri Net Unfolding Algorithm, University of Newcastle upon Tyne, Department of Computing Science, Technical Reports CS-TR-733, Newcastle upon Tyne, UK, June 2001, 14 pp. http://www.cs.ncl.ac.uk/research/pubs/trs/papers/733.pdf

50
Keijo Heljanko and Ilkka Niemelä, ``Petri Net Analysis and Nonmonotonic Reasoning,'' in N. Husberg, T. Janhunen, and I. Niemelä (Eds.), Leksa Notes in Computer Science: Festschrift in Honour of Professor Leo Ojala, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A63, Espoo, October 2000, pp. 7-19. http://www.tcs.hut.fi/~kepa/publications/hn-lncs.ps.gz

51
Tomi Janhunen, ``Specifying Agent-Based Systems with Nets and Logic Programs,'' in N. Husberg, T. Janhunen, and I. Niemelä (Eds.), Leksa Notes in Computer Science: Festschrift in Honour of Professor Leo Ojala, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A63, Espoo, October 2000, pp. 33-46.

52
Tommi Junttila, Computational Complexity of the Place/Transition-Net Symmetry Reduction Method, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A59, Espoo, April 2000, 16 pp. http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A59.shtml

53
Tommi Junttila, New Canonical Representative Marking Algorithms for Place/Transition-Nets, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A75, Espoo, October 2002, 37 pp. http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A75.shtml

54
Tommi Junttila, Symmetry Reduction Algorithms for Data Symmetries, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A72, Espoo, May 2002, 49 pp.
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A72.shtml

55
Timo Latvala, On Model Checking Safety Properties, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports HUT-TCS-A76, Espoo, December 2002, 61 pp.
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A76.shtml