• Groene Loper 5, Metaforum

    5612 AP Eindhoven

    Netherlands

  • P.O. Box 513, Department of Mathematics and Computer Science

    5600 MB Eindhoven

    Netherlands

Research Output 2001 2019

2019
3 Citations (Scopus)

Active learning of industrial software with data

Sanchez, L., Groote, J. F. & Schiffelers, R., 2019, Preproceedings of Fundamentals of Software Engineering (FSEN) 2019. Hojjat, H. & Massink, M. (eds.). Tehran: Institute for Studies in Theoretical Physics and Mathematics (IPM), School of Mathematics, p. 51-65 14 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Learning systems
Large scale systems
Problem-Based Learning

Correct and efficient antichain algorithms for refinement checking

Laveaux, M., Groote, J. F. & Willemse, T., 2019, Eindhoven: Technische Universiteit Eindhoven. 28 p. (Computer science reports; vol. 19/01)

Research output: Book/ReportReportAcademic

Open Access
File
Specifications
Data storage equipment
Experiments

Correct and efficient antichain algorithms for refinement checking

Laveaux, M., Groote, J. F. & Willemse, T. A. C., 26 Feb 2019, In : arXiv. 28 p., 1902.09880

Research output: Contribution to journalArticleAcademic

Open Access
File
Specifications
Data storage equipment
Experiments

Divide and congruence III: from decomposition of modal formulas to preservation of stability and divergence

Fokkink, W. J., van Glabbeek, R. & Luttik, B., 24 Jul 2019, In : Information and Computation. 104435

Research output: Contribution to journalArticleAcademicpeer-review

Preservation
Congruence
Divides
Divergence
Semantics
1 Citation (Scopus)

Lower bounds for synchronizing word lengths in partial automata

de Bondt, M., Don, H. M. & Zantema, H., 2019, In : International Journal of Foundations of Computer Science. 30, 1, p. 29-60 32 p.

Research output: Contribution to journalArticleAcademicpeer-review

Synchronization

Solving computational problems in the theory of word-representable graphs

Akgün, Ö., Gent, I., Kitaev, S. & Zantema, H., 2019, In : Journal of Integer Sequences. 22, 2, 18 p., 19.2.5

Research output: Contribution to journalArticleAcademicpeer-review

Graph in graph theory
Representability
Comparability Graph
Graph Representation
Odd number

The k-dimensional cube is k-representable

Broere, B. & Zantema, H., 2019, In : Journal of Automata, Languages and Combinatorics. 24, 1, p. 3-12 10 p.

Research output: Contribution to journalArticleAcademicpeer-review

Regular hexahedron
Cartesian product
Vertex of a graph
Product Graph
Concatenation

Verification of hypertorus communication grids by infinite Petri nets and process algebra

Zaitsev, D., Shmeleva, T. & Groote, J. F., 2019, In : IEEE/CAA Journal of Automatica Sinica. 6, 3, p. 733-742 10 p.

Research output: Contribution to journalArticleAcademicpeer-review

Petri nets
Algebra
Communication
Packet switching
Structural analysis

Verifying system-wide properties of industrial component-based software

Neele, T., Rol, M. H. & Groote, J. F., 2019, Pre proceedings of Fundamentals of Software Engineering 2019. Hojjat, H. & Massink, M. (eds.). Teheran: Institute for Studies in Theoretical Physics and Mathematics (IPM), School of Mathematics, p. 5-20 16 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Software design
Engines
2018

A comparison of BDD-based parity game solvers

Sanchez, L., Wesselink, W. & Willemse, T. A. C., 7 Sep 2018, Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification. Waterloo: Open Publishing Association, p. 103-117 15 p. (Electronic Proceedings in Theoretical Computer Science ; vol. 27)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Open Access
1 Citation (Scopus)

An efficient algorithm to determine probabilistic bisimulation

Groote, J. F., Rivera Verduzco, H. J. & de Vink, E. P., 5 Sep 2018, In : Algorithms. 11, 9, 22 p., 131

Research output: Contribution to journalArticleAcademicpeer-review

Open Access
File
Bisimulation
Efficient Algorithms
Labeled Transition System
Systems science
Transition Systems

Automatic generation of hardware checkers from formal micro-architectural specifications

Fedotov, A. & Schmaltz, J., 19 Apr 2018, Proceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018. Institute of Electrical and Electronics Engineers, Vol. 2018-January, p. 1568-1573 6 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Specifications
Hardware
Computer hardware description languages
Inclusion
Functionality

BDD-based parity game solving: a comparison of Zielonka's recursive algorithm, priority promotion and fixpoint iteration

Sanchez, L., Wesselink, J. W. & Willemse, T. A. C., 2018, Eindhoven: Technische Universiteit Eindhoven. 19 p. (Computer science reports; vol. 1801)

Research output: Book/ReportReportAcademic

Open Access
File

Counting symbol switches in synchronizing automata

Don, H. M. & Zantema, H., 2018, In : arXiv. 26 p., 1812.04050v1

Research output: Contribution to journalArticleAcademic

Open Access
File
Automata
Counting
Switch
Count
Synchronization
1 Citation (Scopus)

Deadlock detection for actor-based coroutines

Azadbakht, K., de Boer, F. S. & de Vink, E., 1 Jan 2018, Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Havelund, K., Peleska, J., Roscoe, B. & de Vink, E. (eds.). Cham: Springer, p. 39-54 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10951 LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Computability and decidability
Deadlock
Scheduling
Transition Systems
Decidability
2 Citations (Scopus)

Evidence extraction from parameterised Boolean equation systems

Wesselink, W. & Willemse, T. A. C., 1 Jan 2018, Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018): Oxford, UK, July 18, 2018.. Benzmüller, C. & Otten, J. (eds.). CEUR-WS.org, p. 86-100 15 p. (CEUR Workshop Proceedings; vol. 2095)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Open Access
File
Model checking
Feedback
Hardware

Extending paradigm with data

Groenewegen, L. P. J., Verschuren, J. H. S. & de Vink, E. P., 1 Jan 2018, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). de Boer, F., Bonsangue, M. & Rutten, J. (eds.). Dordrecht: Springer, p. 224-244 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10865 LNCS)

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

Bakeries
Paradigm
Dependent Data
Modeling Language
Interaction

Finding small counter examples for abstract rewriting properties

Zantema, H., 1 Sep 2018, In : Mathematical Structures in Computer Science. 28, 8, p. 1485-1505 21 p.

Research output: Contribution to journalArticleAcademicpeer-review

Open Access
File
Rewriting
Counterexample
Binary relation
Theorem
Termination

Formal methods: 22nd international symposium, FM 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, proceedings

Havelund, K. (ed.), Peleska, J. (ed.), Roscoe, B. (ed.) & de Vink, E. (ed.), 2018, Cham: Springer. (Lecture Notes in Computer Science; vol. 10951)(Programming and software engineering; vol. 10951)

Research output: Book/ReportBook editingAcademicpeer-review

Formal micro-architectural analysis of on-chip ring networks

van Wesel, P. & Schmaltz, J., 24 Jun 2018, Proceedings of the 55th Annual Design Automation Conference, DAC 2018. New York: ACM/IEEE, 6 p. 94

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Ring Network
Deadlock
Chip
Ring
Formal Modeling

Logistics modeling and analysis for chuck exchange using Product Line Engineering

Fekade Yimam, B., 24 Oct 2018, Eindhoven: Technische Universiteit Eindhoven. 57 p.

Research output: ThesisPd Eng ThesisAcademic

Open Access
File

Lower bounds for synchronizing word lengths in partial automata

de Bondt, M., Don, H. M. & Zantema, H., 2018, In : arXiv. 1801.10436

Research output: Contribution to journalArticleAcademic

Open Access
File
Automata
Lower bound
Partial
Series
Rewriting
1 Citation (Scopus)

Modelling and analysing ERTMS hybrid level 3 with the mCRL2 toolset

Bartholomeus, M., Luttik, B. & Willemse, T., 1 Jan 2018, Formal Methods for Industrial Critical Systems - 23rd International Conference, FMICS 2018, Proceedings. Howar, F. & Barnat, J. (eds.). Berlin: Springer, p. 98-114 17 p. (Lecture Notes in Computer Science; vol. 11119)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Specification
Specifications
Process Algebra
Global system for mobile communications
Railway
1 Citation (Scopus)

Pitfalls in applying model learning to industrial legacy software

al Duhaiby, O., Mooij, A., van Wezep, H. & Groote, J. F., 30 Oct 2018, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings. Margaria, T. & Steffen, B. (eds.). Cham: Springer, p. 121-138 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11247 LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Software
Model
Healthcare
Open Problems
Industry

Scalable performance analysis of wireless sensor networks

Talebi, M., 25 Oct 2018, Eindhoven: Technische Universiteit Eindhoven. 137 p.

Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)Academic

Open Access
File
1 Citation (Scopus)

Solving parameterised boolean equation systems with infinite data through quotienting

Neele, T., Willemse, T. A. C. & Groote, J. F., 5 Oct 2018, Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings. Ölveczky, P. C. & Bae, K. (eds.). Berlin: Springer, p. 216-236 21 p. (Lecture Notes in Computer Science; vol. 11222)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Model checking
Equivalence Problem
Bisimulation
Decision problem
Model Checking
1 Citation (Scopus)

Synchronizing non-deterministic finite automata

Don, H. & Zantema, H., 2018, In : Journal of Automata, Languages and Combinatorics. 23, 4, p. 307-328 22 p.

Research output: Contribution to journalArticleAcademicpeer-review

Open Access
File
Finite Automata
Finite automata
Upper bound
Sharp Bound
Imply
2017

A formalisation of consistent consequence for boolean equation systems

van Delft, M., Geuvers, H. & Willemse, T. A. C., 2017, Interactive theorem proving - 8th International Conference, ITP 2017,Proceedings. Ayala-Rincón, M. & Muñoz, C. A. (eds.). Springer, p. 462-478 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10499)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Formalization
Acoustic waves
Boolean algebra
Model checking
Boolean Lattice
11 Citations (Scopus)

An O(mlog n) algorithm for computing stuttering equivalence and branching bisimulation

Groote, J. F., Jansen, D. N., Keiren, J. J. A. & Wijs, A. J., 1 Jun 2017, In : ACM Transactions on Computational Logic. 18, 2, 13

Research output: Contribution to journalArticleAcademicpeer-review

Bisimulation
Branching
Equivalence
Computing
Time Complexity

Assessing the quality of tabular state machines through metrics

Osaiweran, A. A. H., Marincic, J. & Groote, J. F., 2017, Eindhoven: Technische Universiteit Eindhoven. 16 p. (Computer science reports; vol. 1701)

Research output: Book/ReportReportAcademic

Open Access
File

Assessing the quality of tabular state machines through metrics.

Osaiweran, A. A. H., Marincic, J. & Groote, J. F., 2017, Proceedings of the 2017th IEEE International Conferenence on Software Quality, Reliability and Security. Piscataway: IEEE Press, p. 426-433 8 p. 8009946

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Software design
Industry
1 Citation (Scopus)

Brzozowski goes concurrent: A Kleene Theorem for pomset languages

Kappé, T., Brunet, P., Luttik, S. P., Silva, A. & Zanasi, F., 2017, 28th International Conference on Concurrency Theory (CONCUR 2017). Meyer, R. & Nestmann, U. (eds.). Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, p. 1-16 16 p. 25. (Leibniz International Proceedings in Informatics (LIPIcs); vol. 85)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Open Access
File
Kleene Algebra
Automata
Concurrent
Theorem
Language

Classifying non-periodic sequences by permutation transducers

Zantema, H. & Bosma, W., 2017, Developments in Langauge Theory"21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings. Charlier, E., Leroy, J. & Rigo, M. (eds.). Cham: Springer, p. 365-377 13 p. (Lecture Notes in Computer Science ; vol. 10396)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Transducer
Permutation
Strictly
Polynomial
Hierarchy

Deriving natural deduction rules from truth tables

Geuvers, H. & Hurkens, T., 1 Jan 2017, Logic and Its Applications - 7th Indian Conference, ICLA 2017, Proceedings. Ghosh, S. & Prasad, S. (eds.). Berlin: Springer, p. 123-138 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10119 LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Truth table
Natural Deduction
Textbooks
Semantics
Acoustic waves
4 Citations (Scopus)

DFAs and PFAs with long shortest synchronizing word length

de Bondt, M., Don, H. & Zantema, H., 2017, Developments in Language Theory : 21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings. Charlier, E., Leroy, J. & Rigo, M. (eds.). Dordrecht: Springer, p. 122-133 12 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10396 LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Arbitrary
4 Citations (Scopus)

Divide and congruence III: stability & divergence

Fokkink, W., van Glabbeek, R. & Luttik, B., 1 Aug 2017, 28th International Conference on Concurrency Theory, CONCUR 2017. Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Vol. 85, 16 p. 15

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Open Access
File
Semantics
Decomposition

Family-based model checking of SPL with mCRL2

Snaiba, Z. B., De Vink, E. P. & Willemse, T. A. C., 25 Sep 2017, SPLC '17 Proceedings of the 21st International Systems and Software Product Line Conference, 25-29 September 2017, Sevilla, Spain. New York: Association for Computing Machinery, Inc, Vol. B, p. 13-16 4 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Model checking
Specifications
11 Citations (Scopus)

Family-based model checking with mCRL2

ter Beek, M. H., de Vink, E. P. & Willemse, T. A. C., 2017, Fundamental Approaches to Software Engineering: 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Huisman, M. & Rubin, J. (eds.). Dordrecht: Springer, p. 387-405 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10202 LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Model checking
Software Product Lines
Model Checking
μ-calculus
Benchmark
2 Citations (Scopus)

Finding DFAs with maximal shortest synchronizing word length

Zantema, H. & Don, H., 2017, Language and Automata Theory and Applications: 11th International Conference, LATA 2017, Umeå, Sweden, March 6-9, 2017, Proceedings. Drewes, F., Martín-Vide, C. & Truthe, B. (eds.). Dordrecht: Springer, p. 249-260 12 p. (LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)

Formalising the Dezyne modelling language in mCRL2

van Beusekom, R., Groote, J. F., Hoogendijk, P., Howe, R., Wesselink, W., Wieringa, R. & Willemse, T. A. C., 2017, Critical Systems: Formal Methods and Automated Verification: Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings. Petrucci, L., Seceleanu, C. & Cavalcanti, A. (eds.). Dordrecht: Springer, p. 217-233 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10471 LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Modeling Language
Model Transformation
Model checking
Model Checking
Refinement
1 Citation (Scopus)

Games for bisimulations and abstraction

de Frutos Escrig, D., Keiren, J. J. A. & Willemse, T. A. C., 22 Nov 2017, In : Logical Methods in Computer Science. 13, 4, 40 p., 15

Research output: Contribution to journalArticleAcademic

Open Access
File
Bisimulation
Game
Specification
Specifications
Process Algebra

Modelling and verification of a cluster-tree formation protocol implementation for the IEEE 802.15.4 TSCH MAC operation mode.

Talebi, M., Groote, J. F. & Dandelski, C., 2017, Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017). Hermanns, H. & Höfner, P. H. (eds.). p. 117-128

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Open Access
File
Topology
Network protocols
Formal methods
Wireless ad hoc networks
Wireless sensor networks
2 Citations (Scopus)

Ordering sequences by permutation transducers

Bosma, W. & Zantema, H., 1 Feb 2017, In : Indagationes Mathematicae. 28, 1, p. 38-54 17 p.

Research output: Contribution to journalArticleAcademicpeer-review

Open Access
Transducer
Permutation
Equivalence class
Periodic Sequence
Automata
1 Citation (Scopus)

Parity game reductions

Cranen, S., Keiren, J. J. A. & Willemse, T. A. C., 4 Aug 2017, In : Acta Informatica. 55, 5, p. 401-444 44 p.

Research output: Contribution to journalArticleAcademicpeer-review

Open Access
File
Model checking

Problem solving using process algebra considered insightful

Groote, J. F. & de Vink, E. P., 2017, Eindhoven: Technische Universiteit Eindhoven. 13 p. (Computer science reports; vol. 1702)

Research output: Book/ReportReportAcademic

Open Access
File
3 Citations (Scopus)

Problem solving using process algebra considered insightful.

Groote, J. F. & de Vink, E. P., 2017, ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday. Katoen, J-P., Langerak, R. & Rensink, A. (eds.). Cham: Springer, p. 48-63 (Lecture Notes in Computer Science; vol. 10500)

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

Process Algebra
Combinatorial Problems
Model Checking
Visualization
Model

Proceedings 15th workshop on Quantitative Aspects of Programming Languages and systems (QAPL 2017): Uppsala, Sweden, 23rd April 2017

Wiklicky, H. & de Vink, E. P., 2017, Electronic Proceedings in Theoretical Computer Science ed. Uppsala. 126 p.

Research output: Book/ReportBook editingAcademicpeer-review

Open Access
Computer programming languages
Semantics
Satellites
Bandwidth
4 Citations (Scopus)

Refinement-aware generation of attack trees

Gadyatskaya, O., Jhawar, R., Mauw, S., Trujillo-Rasua, R. & Willemse, T. A. C., 2017, Security and Trust Management: 13th International Workshop, STM 2017, Oslo, Norway, September 14–15, 2017, Proceedings. Livraga, G. & Mitchell, C. (eds.). Dordrecht: Springer, p. 164-179 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10547 LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Refinement
Attack
Processing
Vulnerability
Methodology
1 Citation (Scopus)

Sequential composition in the presence of intermediate termination: (Extended Abstract)

Baeten, J. C. M., Luttik, S. P. & Yang, F., 2017, Proceedings of the Combined 24th International Workshop on Expressiveness in Concurrency, Berlin, Germany, 4th September 2017. Peters, K. & Tini, S. (eds.). p. 1-17 17 p. (EPTCS; vol. 255)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Open Access
File
Semantics
Chemical analysis
Transparency
1 Citation (Scopus)

Termination of cycle rewriting by transformation and matrix interpretation

Sabel, D. & Zantema, H., 1 Jan 2017, In : Logical Methods in Computer Science. 13, 1, 11

Research output: Contribution to journalArticleAcademicpeer-review

Open Access
File
Rewriting
Termination
Acoustic waves
Cycle
Strings