Current research topics
and papers published after 2000
Causal process
semantics of concurrent systems
Occurrence nets are representatives
of single runs of a Petri net, which are suitable for describing explicit causality
and concurrency. In this work we extended the causal process semantics to Petri
nets with inhibitor arcs and then nets with localities. We also developed an
extension of casual processes to gain
better understanding of complex fault-error-failure chains.
Structured Occurrence Nets: A Formalism for Aiding System
Failure Prevention and Analysis Techniques, Koutny, M. and Randell,
B., Fundamenta Informaticae, Volume 97, Issue 1-2, pp 41-91,
IOS Press, ISSN: 0169-2968, 2009
Formal Languages and Concurrent Behaviours, , In: New
Developments in Formal Languages and Applications, Bel-Enguix, G., Jiménez-López, M.D. and Martín-Vide,
C. (eds), Studies in Computational Intelligence,
Volume 113, pp 125-182, 2008
Processes of
Petri Nets with Range Testing, Kleijn, J. and Koutny, M., Fundamenta
Informaticae, Volume 80, Issue 1-3, pp 199-219,
IOS Press, ISSN: 0169-2968, 2007
Failures: Their
Definition, Modelling and Analysis, Randell, B. and
Koutny, M., In Theoretical Aspects of Computing - ICTAC 2007, 4th International
Colloquium, Jones, C.B., Liu, Z. and Woodcock, J. (eds.) Lecture Notes in Computer Science, Volume 4711, pp 260-274,
Springer-Verlag 2007
Infinite Process
Semantics of Inhibitor Nets, Kleijn, H.C.M. and Koutny, M., In 27th
International Conference on Applications and Theory of Petri Nets and Other
Models of Concurrency, Donatelli, S. and Thiagarajan,
P. S. (eds.) Lecture Notes in Computer Science, Volume 4024, pp 282-301,
Springer-Verlag 2006
Process Semantics
of General Inhibitor Nets, Kleijn, H.C.M. and Koutny, M., Information and
Computation, Volume 190, Issue 1, pp 18-69, Elsevier Science Publishers BV
2004
Causality
Semantics of Petri Nets with Weighted Inhibitor Arcs, Kleijn, H.C.M. and
Koutny, M., In 13th International Conference on Concurrency Theory (CONCUR
2002), Brim, L., Jancar, P., Kretínský,
M. and Kucera, A. (eds.) Lecture Notes in Computer
Science, Volume 2421, pp 531-546, Springer-Verlag
2002
Process Semantics
of P/T-Nets with Inhibitor Arcs, Kleijn, H.C.M. and Koutny, M., In 21st
International Conference on Application and Theory of Petri Nets (ICATPN 2000),
Nielsen, M. and Simpson, D. (eds.) Lecture
Notes in Computer Science, Volume 1825, pp 261-281, Springer-Verlag 2000
Concurrency
models: unification of Petri nets and process algebras
The standard
treatment of the structure and semantics of concurrent systems provided by
process algebras and Petri nets is different, making it difficult to take full
advantage of their relative strengths. We achieved a unification of basic
classes of Petri nets and process algebras. This has been later extended to
deal with asynchronous message passing and mobility.
A
Compositional Petri Net Translation of General pi-calculus Terms, , Formal Aspects of Computing, Volume 20,
pp 429-450, 2008
Modelling Mobility in
High-level Petri Nets, Devillers, R., Klaudel, H. and
Koutny, M., In Seventh International Conference on Application of Concurrency
to System Design, ACSD 2007, Basten, T., Juhas, G. and Shukla, S. (eds.)
pp 110-119, IEEE Computer Society 2007
A
Petri Net Translation of p-Calculus Terms, Devillers,
R., Klaudel, H. and Koutny, M., In Theoretical Aspects of Computing - ICTAC
2006. Barkaoui, K., Cavalcanti, A. and Cerone, A. (eds.) Lecture Notes in Computer Science,
Volume 4281, pp 138-152, Springer-Verlag 2006
A
Petri Net Semantics of a Simple Process Algebra for Mobility, Devillers, R., Klaudel, H. and Koutny, M., Electronic
Notes in Theoretical Computer Science, Volume 154, Issue 3, pp 71-94,
Elsevier B.V., 2006
Context-Based
Process Algebras for Mobility, Devillers, R.,
Klaudel, H. and Koutny, M., In 4th International Conference on Application of
Concurrency to System Design (ACSD 2004), Kishinevsky
M. and Darondeau, Ph. (eds.) pp 79-88, IEEE Computer Society 2004
Process
Algebra: A Petri-Net-Oriented Tutorial Best, E., and Koutny, M., In: Lectures
on Concurrency and Petri Nets: Advances in Petri Nets, Desel,
J., Reisig, W., and Rozenberg, G. (ed), pp 180-209, Series: Lecture
Notes in Computer Science, Volume 3098, Springer-Verlag,
ISBN: 3-540-22261-8, 2004
Asynchronous
Box Calculus, Devillers, R., Klaudel, H., Koutny, M.
and Pommereau, F., Fundamenta Informaticae, Volume 54, Issue 4, pp 295-344, IOS
Press, ISSN: 0169-2968, 2003
Compositional
Development In the Event of Interface Difference
The
Box Algebra = Petri Nets + Process Expressions, Best, E., Devillers,
R. and Koutny, M., Information and Computation, Volume 178, Issue 1, pp
44-100, Academic Press, ISSN: 0890-5401, 2002
An
Algebra of Non-safe Petri Boxes, Devillers, R.,
Klaudel, H., Koutny, M. and Pommereau, F., In 9th International Conference on
Algebraic Methodology and Software Technology (AMAST 2002), Kirchner, H. and Ringeissen, C. (eds.) Lecture Notes in Computer Science,
Volume 2422, pp 192-207, Springer-Verlag 2002
Petri
Net Algebra, Best, E., Devillers, R.
and Koutny, M., Series: Monographs in Theoretical Computer Science: An EATCS
Series, Springer-Verlag, ISBN: 3-540-67398-9, 2001
A
Unified Model for Nets and Process Algebras Best, E., Devillers,
R. and Koutny, M., In: Handbook of Process Algebra, Bergstra,
J., Ponse, A. and Smolka,
S. (eds.) pp 873-944, Elsevier Science Publishers BV, ISBN: 0-444-82830-3, 2001
Recursion
and Petri Nets, Best, E., Devillers, R. and Koutny,
M., Acta Informatica,
Volume 37, Issue 11-12, pp 781-829, Springer-Verlag,
ISSN: 0001-5903, 2001
A
Compositional Model of Time Petri Nets, Koutny, M., In 21st International
Conference on Application and Theory of Petri Nets (ICATPN 2000), Nielsen, M.
and Simpson, D. (eds.) Lecture Notes in Computer Science, Volume 1825,
pp 303-322, Springer-Verlag 2000
Framed temporal logic programming
This
work is concerned with various syntactic and semantic aspects of an executable
temporal logic programming language, called Framed Tempura. It is based on the
projection temporal logic and some of its laws are investigated. A synchronous
communication mechanism for concurrent programs is provided by means of the
framing technique and minimal model semantics.
Framed
Temporal Logic Programming, Duan, Z., Yang, X. and Koutny, M., Science of
Computer Programming, Volume 70, Issue 1, pp 31-61, Elsevier Science
Publishers BV 2008
Semantics of Framed Temporal Logic Programs, Duan, Z.,
Yang, X. and Koutny, M., In Logic Programming. 21st
International Conference, ICLP 2005, Gabbrielli, M.
and Gupta, G. (eds.) Lecture Notes in Computer Science, Volume 3668, pp
356-370, Springer-Verlag 2005
A
Framed Temporal Logic Programming Language, Duan, Z.-H., Koutny, M., Journal
of Computer Science and Technology, Volume 19, Issue 3, pp 341-351, Allerton Press, Inc. 2004
Information flow analysis through opacity
Opacity is a technique for
describing security properties in information flow. It captures properties of
the local states of the secure (or high-level) part of the system, based on the
observation of the local states of a low-level part of the system as well as
observed actions. We first formalised opacity as a
Petri net modelling technique and then extended it to
general labelled transition systems. We established
links between opacity and anonymity and non-inference, and also investigated
ways of verifying opacity.
Opacity
generalised to transition systems, , International
Journal of Information Security, Volume 7,
pp 421-435, 2008
Opacity
Generalised to Transition Systems, Bryans, J.W.,
Koutny, M., Mazaré, L. and Ryan, P.Y.A., In Formal
Aspects in Security and Trust. Third International Workshop,
FAST 2005, Dimitrakos. T., Martinelli,
F., Ryan, P.Y.A. and Schneider, S. (eds.) Lecture Notes in Computer Science,
Volume 3866, pp 81-95, Springer-Verlag 2006
Modelling Opacity Using
Petri Nets, Bryans, J.W., Koutny, M. and Ryan P.Y.A., Electronic Notes in
Theoretical Computer Science, Volume 121, pp 101-115, Elsevier Science
Publishers BV 2005
Modelling Dynamic
Opacity using Petri Nets with Silent Actions,
Model-checking using net unfoldings
The group has
achieved notable advances in tool support for applicable modelling
and reasoning approaches, contributing high performance model-checking tools
for software and hardware verification. Techniques for checking behavioural properties of concurrent systems have been
developed using Petri Net unfoldings and other highly
condensed representations, integer programming and SAT-based techniques. In the
area of hardware verification, fast SAT-based methods have been used for
detecting state encoding conflicts in specifications and for logic synthesis of
asynchronous circuits, as well as visualisation of
concurrent behaviours.
Verification
of Bounded Petri Nets Using Integer Programming, Khomenko, V. and Koutny, M., Formal
Methods in System Design, Volume 30, Issue 2, pp 143-176, Springer-Verlag 2007
Merged
Processes: a New Condensed Representation of Petri Net Behaviour,
Khomenko, V., Kondratyev, A., Koutny, M. and Vogler, W., Acta Informatica, Volume 43, Issue 5, pp 307-330, Springer-Verlag 2006
also in: In CONCUR 2005 - Concurrency Theory. 16th
International Conference, Abadi, M. and de Alfaro, L.
(eds.) Lecture Notes in Computer Science, Volume 3653, pp 338-352,
Springer-Verlag 2005
Branching
Processes of High-Level Petri Nets, Khomenko, V. and Koutny, M., In 9th
International Conference on Tools and Algorithms for the Construction and
Analysis of Systems (TACAS 2003), Garavel, H. and Hat
Canonical
Prefixes of Petri Net Unfoldings, Khomenko, V.,
Koutny M. and Vogler W., Acta
Informatica, Volume 40, pp 95-118, Springer-Verlag 2003
also in: 14th
International Conference on Computer Aided Verification (CAV 2002), Brinksma E. and Larsen K.G. (eds.) Lecture Notes in
Computer Science, Volume 2404, pp 582-595, Springer-Verlag
2002
Parallelisation of the Petri Net Unfolding Algorithm, Heljanko, K., Khomenko, V. and Koutny, M., In 8th
International Conference on Tools and Algorithms for the Construction and
Analysis of Systems (TACAS 2002), Katoen, J.-P. and Stevens, P. (eds.) Lecture Notes in Computer Science,
Volume 2280, pp 371-385, Springer-Verlag 2002
Towards
an Efficient Algorithm for Unfolding Petri Nets, Khomenko, V. and Koutny, M.,
In 12th International Conference on Concurrency Theory (CONCUR 2001), Larsen,
K.G. and Nielsen, M. (eds.) Lecture Notes in Computer Science, Volume
2154, pp 366-380, Springer-Verlag 2001
LP
Deadlock Checking Using Partial Order Dependencies, Khomenko, V. and Koutny,
M., In 11th International Conference on Concurrency Theory (CONCUR 2000), Palamidessi, C. (ed) Lecture Notes in Computer Science,
Volume 1877, pp 410-425, Springer-Verlag 2000
Relating communicating processes with
different interfaces
It is often desirable to describe the
interface of an implementation system at a different (usually more detailed)
level of abstraction to the interface of the relevant specification. We
developed an approach to deal with behaviour
abstraction in networks of communicating processes which is, in particular,
suitable for compositional verification.
Compositional
Abstractions for Process Networks, , IADIS International Journal on Computer Science and Information Systems,
Volume 3, pp 71-85, 2008
Towards an
Algebra of Abstractions for Communicating Processes, Koutny, M., Pappalardo, G. and Pietkiewicz-Koutny,
M., In Sixth International Conference on Application of Concurrency to System
Design (ACSD 2006), Goossens, K. and Petrucci, L. (eds.) pp 239-250, IEEE Computer Society 2006
Relating
Communicating Processes with Different Interfaces,
Behaviour Abstraction for Communicating Sequential Processes,
Koutny, M. and Pappalardo, G., Fundamenta
Informaticae, Volume 48, Issue 1, pp 21-54, IOS
Press, ISSN: 0169-2968, 2001
Verifying
Implementation Relations in the Event of Interface Difference, Burton, J., Koutny,
M. and Pappalardo, G., In International Symposium of
Formal Methods Europe, FME 2001: Formal Methods for Increasing Software
Productivity, Oliveira, J.N. and Zave, P. (eds.) Lecture
Notes in Computer Science, Volume 2021, pp 364-383, Springer-Verlag 2001
Implementing
Communicating Processes in the Event of Interface Difference, Burton, J.,
Koutny, M. and Pappalardo, G., In 2nd International
Conference on Application of Concurrency to System Design (ACSD 2001), Valmari, A. and Yakovlev, A. (eds.) pp 87-98, IEEE Computer
Society Press 2001
Semantics of membrane systems
Using
nets with explicit localities we developed a causal process model describing
the structure of the behaviour of membrane systems. Each locality identifies a
distinct set of transitions which may only be executed synchronously in a
locally maximal concurrent manner.
Petri
Nets and Membrane Computing, Kleijn, J and Koutny, M., In The Oxford Handbook
of Membrane Computing, Paun, G., Rozenberg,
G. and Salomaa, A.(eds.),
2010
Steps
and Coverability in Inhibitor Nets, Kleijn, J and
Koutny, M., In Perspectives in Concurrency Theory, Lodaya,
K., Mukund, M. and Ramanujam,
R.(eds.), Universities Press, pp 264-295, 2009
A
Petri net model for membrane systems with dynamic structure, , Natural Computing, Springer, Online: October 01, 2008
Processes of Membrane Systems with Promoters and Inhibitors, Kleijn, J. and Koutny, M., Theoretical Computer Science, Volume 404, pp 112-126, 2008
Process Semantics for Membrane Systems,
Kleijn, J., Koutny, M. and Rozenberg, G., Journal of Automata, Languages and
Combinatorics, Volume 11, Issue 3, pp 321–340,
2006
Synchrony and
Asynchrony in Membrane Systems, Kleijn, J. and Koutny, M., In Membrane
Computing. 7th
International Workshop, WMC 2006, Hoogeboom, H.J., Paun, G., Rozenberg, G. and Salomaa,
A. (eds.) Lecture Notes in Computer Science, Volume 4361, pp 66-85, Springer-Verlag
2006
Towards a Petri Net Semantics for
Membrane Systems, Kleijn, H.C.M., Koutny, M. and Rozenberg, G., In Membrane
Computing: 6th International Workshop, WMC 2005, Vienna, Austria, July 18-21,
2005 Freund, R., Paun, G., Rozenberg, G. and Salomaa, A. (eds.) Lecture Notes in Computer Science,
Volume 3850, pp 292-309, Springer-Verlag 2006
Synthesis of concurrent systems
We investigated
the following version of the synthesis problem: given a transition system
representing the desired behaviour, derive a Petri
net which generates this transition system. Recently, we provided a new
solution for this problem for Petri nets with localities. This has led to a
proposal of a new model of concurrent behaviour
involving Petri nets (providing the structure of a system) and execution
policies additionally constraining their dynamic behaviour
(such as maximal concurrency).
Synthesis of Nets with Step Firing Policies, , Fundamenta Informaticae,
Volume 94, 2009
Synthesis of Petri Nets with Localities, Koutny, M., Pietkiewicz-Koutny,
M., Scientific Annals of Computer
Science, Volume 19, pp 1-23, 2009
Minimal Regions of ENL-transition Systems, Koutny, M., Pietkiewicz-Koutny,
M., Concurrency, Specification, and Programming, CS&P 2009, pp 303-314,
2009
Synthesis of PTL-nets with Partially Localised Conflicts,
Koutny, M., Pietkiewicz-Koutny, M., International
Workshop on Petri Nets and Software Engineering, PNSE'09, pp 247-254, 2009
Synthesis of Elementary Net Systems with Context Arcs and Localities, , Fundamenta Informaticae, Volume 88, pp 307-328, 2008
Synthesis of Nets with Step Firing Policies, , In Applications and Theory of Petri Nets. 29th International Conference, PETRI NETS 2008, van Hee, K.M. and Valk,
R. (eds.), Lecture
Notes in Computer Science, Volume 5062, pp
112-131, 2008
Synthesis
of Elementary Net Systems with Context Arcs and Localities, Koutny, M. and Pietkiewicz-Koutny, M., In 28th International Conference on
Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN
2007, Kleijn, J. and Yakovlev, A. (eds.) Lecture Notes in Computer Science,
Volume 4546, pp 281-300, Springer-Verlag 2007
Transition
Systems of Elementary Net Systems with Localities, Koutny, M. and Pietkiewicz-Koutny, M., In 17th International Conference,
CONCUR 2006, Baier, C. and Hermanns,
H. (eds.) Lecture Notes in Computer Science, Volume 4137, pp 173-187,
Springer-Verlag 2006
Verification and synthesis of asynchronous circuits
The
verification techniques based on Petri net unfoldings
and SAT (see above) have been applied to solving various problems arising when
designing asynchronous circuits, such as encoding conflict detection and
resolution.
Logic
Synthesis for Asynchronous Circuits Based on STG Unfoldings
and Incremental SAT, Khomenko, V., Koutny, M. and Yakovlev, A., Fundamenta Informaticae,
Volume 70, Issue 1-2, pp 49-73, IOS Press 2006; also in: Fourth International
Conference on Application of Concurrency to System Design, ACSD 2004, Kishinevsky M. and Darondeau, Ph. (eds.) pp 16-25, IEEE
Computer Society 2004
Detecting
State Encoding Conflicts in STG Unfoldings Using SAT,
Khomenko, V., Koutny, M. and Yakovlev, A., Fundamenta
Informaticae, Volume 62, Issue 2, pp 221-241, IOS
Press 2004; also in: Third International Conference on Application of
Concurrency to System Design, ACSD 2003, Lilius, J., Balarin, F. and Machado, R.J. (eds.) pp 51-60, IEEE
Computer Society 2003
Detecting
State Coding Conflicts in STGs Using Integer Programming, Khomenko, V., Koutny,
M. and Yakovlev, A., In Design, Automation and Test in Europe Conference and
Exposition (DATE 2002), Kloos, C.D. and
Verification of mobile and dynamic systems
A translation of a subset of pi-calculus to high-level
Petri nets have been developed. The resulting nets can be unfolded
using the methods developed by our group, and then efficiently verified.
An
Approach to State Space Reduction for Systems with Dynamic Process Creation,
Klaudel, H., Koutny, M., Pelz, E. and Pommereau, F., 24th International
Symposium on Computer and Information Sciences (ISCIS), IEEE, pp 543-548, 2009
Modelling and
Verification of Timed Interaction and Migration, , In Fundamental Approaches to
Software Engineering. 11th
International Conference, FASE 2008, Fiadeiro, J.L. and Inverardi, P. (eds.), Lecture Notes in Computer
Science, Volume 4961, pp
215-229, 2008
, In Theoretical Aspects of Computing - ICTAC 2008. 5th
International Colloquium, Fitzgerald, J.S., Haxthausen, A.E. and Yenigun, H.
(eds.), Lecture
Notes in Computer Science, Volume 5160, pp 186-200, 2008
Petri
Net Semantics of the Finite p-calculus Terms, Devillers,
R., Klaudel, H. and Koutny, M., Fundamenta Informaticae, Volume 70, Issue 3, pp 203-226, IOS Press
2006
also
in: Formal Techniques for Networked and Distributed Systems-FORTE 2004: 24th
IFIP WG 6.1 International Conference, de Frutos-Escrig,
D. and Nunez, M. (eds.) Lecture Notes in
Computer Science, Volume 3235, pp 309-325, Springer-Verlag
2004
On
Specification and Verification of Location-Based Fault Tolerant Mobile Systems
Iliasov, A., Khomenko, V., Koutny, M. and Romanovsky, A., In: Rigorous
Development of Complex Fault-Tolerant Systems,
Applying Petri Net Unfoldings
for Verification of Mobile Systems, Khomenko, V., Koutny, M. and Niaouris, A., In Fourth International Workshop on Modelling of Objects, Components and Agents.
MOCA'06 Moldt, D. (ed.) pp 161-178, 2006
Edited volumes
Application of Concurrency to System
Design, the Seventh Special Issue, Billington, J., Janicki, R. and Koutny, M.
(eds.), Fundamenta Informaticae,
Volume 95, pp v-viii, 2009
Preface by Guest Editors, Billington,
J. and Koutny, M. (eds.), Transactions
on Petri Nets and Other Models of Concurrency, Volume 3, pp xi-xiii, 2009
CHINA 2008 (Concurrency metHods: Issues aNd
Applications), Kleijn, J. and Koutny, M. (eds.), School of Computing Science,
University of Newcastle upon Tyne, 2008, Proceedings of Workshop held at Xidian University, Xi'an, China, June 2008. Published as: Technical Report no. CS-TR-1102, School of
Computing Science, Newcastle University, 2008
2008 8th International Conference on Application of Concurrency to System Design, Proceedings , June 23-27, 2008, Xi'an, China, Billington, J., Duan, Z. and Koutny, M. (eds.) IEEE Press, 2008
Applications and
Theory of Petri Nets 2001, Proceedings of 22nd International Conference, ICATPN
2001, Colom, J-M. and Koutny, M. (eds.), Lecture Notes in Computer Science, 2075,
Springer-Verlag,
2001