My primary researching area is real-time model checking techniques with specific interests in discrete time properties and model transformation. Most of my work is done in collaboration with my thesis advisor Professor Kim G. Larsen and Assosciate Professor Jiri Srba. As a part of my postgraduate work I was one of the creators of the model checking tool TAPAAL, for verification of Timed-Arc Petri Nets.

You can find me on DBLP and Google Scholar

Scientific Tools

  • TAPAAL - Editor, Simulator and Verification of Timed-Arc Petrinets - (co-founder)
  • opaal - Rapid prototyping tool for experiements for verification of Timed Automata - (co-founder)

Proceedings Publications

  • TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets
    by A. David, L. Jacobsen, M. Jacobsen, K.Y. Jørgensen, M.H. Møller and J. Srba.

  • A Semantic-Preserving Transformation from the Compositional Interchange Format to UPPAAL
    by D.E. Nadales Agut, M.A. Reniers, R.R.H. Schiffelers, K.Y. Jørgensen, and D.A. van Beek.

  • opaal - A Lattice Model Checker
    by Andreas E. Dalsgaard, Rene R. Hansen, Kenneth Yrke Joergensen, Kim G. Larsen, Mads Chr. Olesen, Petur Olsen and Jiri Srba.

  • An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata
    by Joakim Byg, Kenneth Yrke Joergensen and Jiri Srba.

  • TAPAAL: Editor, Simulartor and Verifier of Timed-Arc Petri Nets
    by Joakim Byg, Kenneth Yrke Joergensen and Jiri Srba

Journal Publications

  • TCTL-preserving translations from timed-arc Petri nets to networks of timed automata
    by Joakim Byg, Morten Jacobsen, Lasse Jacobsen, Kenneth Yrke Jørgensen, Mikael Harkjær Møller, Jiří Srba

Book Chapters

  • Tools for Model-Checking Timed Systems
    by A. David, G. Behrmann, P. Bulychev, J. Byg, T. ChatainK, G. Larsen, P. Pettersson, J.I. Rasmussen, J. Srba, W. Yi, K.Y. Jørgensen, D. LimeM. Magnin, O.H. Roux, L.-M. Traonouez

Technical Publications

  • An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata by Joakim Byg, Kenneth Yrke Joergensen and Jiri Srba. Technical report FIMU-RS-2009-06 , Faculty of Informatics MU, 29 pages, 2009.

Master Thesis

  • Regular Model Checking and Verification of Cellular Automata by Joakim Byg and Kenneth Yrke Jørgensen. Department of Computer Science, Aalborg University. 2008. Supervisor: Jiri Srba.