Find Publications

Search concepts
Selected filters
2011
24 Citations (Scopus)

Parametric modal transition systems

Beneš, N., Křetínský, J., Larsen, K. G., Møller, M. H. & Srba, J., 1 Jan 2011, In : Lecture Notes in Computer Science. 6996, p. 275-289 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Transition Systems
Computational complexity
Refinement
Specifications
Reactive Systems
2014
2 Citations (Scopus)

Refinement and Difference for Probabilistic Automata

Larsen, K. G., Delahaye, B., Fahrenberg, U. & Legay, A., 28 Feb 2014, In : Logical Methods in Computer Science. 10, 3, p. 1-32

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
2016
5 Citations (Scopus)

Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization

Jensen, P. G., Larsen, K. G. & Srba, J., 8 Apr 2016, Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Springer, p. 129-146 (Lecture Notes in Computer Science, Vol. 9641).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Petri nets
Controllers
2013
2 Citations (Scopus)

Action Investment Energy Games

Larsen, K. G., Laursen, S. & Srba, J., 2013, Mathematical and Engineering Methods in Computer Science: 8th International Doctoral Workshop, MEMICS 2012, Znojmo, Czech Republic, October 25-28, 2012, Revised Selected Papers. Kučera, A., Henzinger, T. A., Nešetřil, J., Vojnar, T. & Antoš, D. (eds.). Netherlands: Springer Publishing Company, Vol. 7721. p. 155-167 13 p. (Lecture Notes in Computer Science, Vol. 7721).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Costs
2019

Controlling Signalized Intersections using Machine Learning

Eriksen, A. B., Lahrmann, H., Larsen, K. G. & Taankvist, J. H., 2019, In : Transportation Research Procedia.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Learning systems
traffic
Controllers
simulation
road
2016
3 Citations (Scopus)

Limit Your Consumption! Finding Bounds in Average-energy Games

Larsen, K. G., Laursen, S. & Zimmermann, M., 2 Nov 2016, Proceedings 14th International Workshop Quantitative Aspects of Programming Languages and Systems, QAPL'16 2016, Eindhoven, The Netherlands, April 2-3, 2016. Tribastone, M. & Wiklicky, H. (eds.). p. 1-14 14 p. (Electronic Proceedings in Theoretical Computer Science, Vol. 227).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
2012
4 Citations (Scopus)
329 Downloads (Pure)

New Results on Timed Specifications

Bourke, T., David, A., Larsen, K. G., Legay, A., Lime, D., Nyman, U. & Wasowski, A., 23 Feb 2012, Recent Trends in Algebraic Development Techniques: 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers. Mossakowski, T. & Kreowski, H-J. (eds.). Springer, p. 175-192 18 p. (Lecture Notes in Computer Science, Vol. 7137).

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

Open Access
File
2011
85 Citations (Scopus)

Time for Statistical Model Checking of Real-Time Systems

David, A., Larsen, K. G., Legay, A., Mikucionis, M. & Wang, Z., 1 Jan 2011, In : Lecture Notes in Computer Science. 6806 LNCS, p. 349-355 7 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Model checking
Real time systems
Model Checking
Statistical Model
Real-time
2019
1 Citation (Scopus)

Converging from branching to linear metrics on Markov chains

Bacci, G., Bacci, G., Larsen, K. G. & Mardare, R., Jan 2019, In : Mathematical Structures in Computer Science. 29, Special Issue 1, p. 3-37 35 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Markov processes
Branching
Markov chain
Semantics
Linear Time
2011
39 Citations (Scopus)

Quantitative analysis of real-time systems using priced timed automata

Bouyer, P., Fahrenberg, U., Larsen, K. G. & Markey, N., 1 Sep 2011, In : Communications of the A C M. 54, 9, p. 78-87 10 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Real time systems
Chemical analysis
16 Citations (Scopus)

New Results on Abstract Probabilistic Automata

Delahaye, B., Katoen, J-P., Larsen, K. G., Legay, A., Pedersen, M. L., Sher, F. & Wasowski, A., 2011, In : Proceedings of the International Conference on Application of Concurrency to System Design. p. 118-127

Research output: Contribution to journalConference article in JournalResearchpeer-review

10 Citations (Scopus)

Modular Markovian logic

Cardelli, L., Larsen, K. G. & Mardare, R., 1 Jan 2011, In : Lecture Notes in Computer Science. 6756 LNCS, p. 380-391 12 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Logic
Markov processes
Separation Logic
Bisimulation
Axiomatization
2012
10 Citations (Scopus)

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example

Zhao, H., Zhan, N., Kapur, D. & Larsen, K. G., 2012, FM 2012: Formal Methods: 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. Springer, Vol. 7436. p. 471-485 (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2015
15 Citations (Scopus)

Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools

Kim, J. H., Larsen, K. G., Nielsen, B., Mikučionis, M. & Olsen, P., 2015, Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015 Oslo, Norway, June 22-23, 2015 Proceedings. Núñez, M. & Güdemann, M. (eds.). Springer, p. 47-61 (Lecture Notes in Computer Science; No. 9128).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2012
9 Citations (Scopus)

Consistency and Refinement for Interval Markov Chains

Delahaye, B., Larsen, K. G., Legay, A., Pedersen, M. L. & Wasowski, A., 2012, In : Journal of Logic and Algebraic Programming. 81, 3, p. 209-226

Research output: Contribution to journalJournal articleResearchpeer-review

2017
4 Citations (Scopus)

On the Metric-Based Approximate Minimization of Markov Chains

Bacci, G., Bacci, G., Larsen, K. G. & Mardare, R., 2017, In : Leibniz International Proceedings in Informatics. 80, 44, p. 1 14 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
Markov processes
Experiments
2011
14 Citations (Scopus)

Decision Problems for Interval Markov Chains

Delahaye, B., Larsen, K. G., Legay, A., Pedersen, M. L. & Wasowski, A., 2011, In : Lecture Notes in Computer Science. 6638, p. 274-285

Research output: Contribution to journalConference article in JournalResearchpeer-review

2014
479 Downloads (Pure)

Schedulability and Energy Efficiency for Multi-core Hierarchical Scheduling Systems

Boudjadar, J., David, A., Kim, J. H., Larsen, K. G., Nyman, U. & Skou, A., 2014, Proceedings of ERTS2 2014. p. 1-4 4 p.

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

File
2011
1 Citation (Scopus)

Monitoring Dynamical Signals While Testing Timed Aspects of a System

Frehse, G., Larsen, K. G., Mikucionis, M. & Nielsen, B., 1 Jan 2011, In : Lecture Notes in Computer Science. 7019 LNCS, p. 115-130 16 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Monitoring
Hybrid Automata
Testing
Nondeterminism
Timed Automata
2019

Analyzing spreadsheets for parallel execution via model checking

Bøgholm, T., Larsen, K. G., Muniz, M., Thomsen, B. & Thomsen, L. L., 2019, Essays on the Occasion of Bernhard Steffen's 60th Birthday: Models, Mindsets, Meta: The What, the How, and the Why Not?.. Springer, Vol. 11200. p. 27-35 (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
Spreadsheets
Model checking
Parallel programming
Scalability
Derivatives
2016
182 Downloads (Pure)

Energy-Aware Scheduling of FIR Filter Structures using a Timed Automata Model

Wognsen, E. R., Hansen, R. R., Larsen, K. G. & Koch, P., 20 Apr 2016, 2016 IEEE 19th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS). IEEE, p. 163-168 6 p.

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

File
2018

Reachability problems: Special issue

Larsen, K. G., Potapov, I. & Srba, J., 30 Nov 2018, In : Theoretical Computer Science. 750, p. 1

Research output: Contribution to journalEditorialResearchpeer-review

2016
14 Citations (Scopus)

Statistical Model Checking: Past, Present, and Future

Larsen, K. G. & Legay, A., 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. Springer, p. 3–15 (Lecture Notes in Computer Science, Vol. 9952).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2019

Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs

Jaeger, M., Jensen, P. G., Larsen, K. G., Legay, A. B. E., Sedwards, S. & Taankvist, J. H., 28 Oct 2019, LNCS: ATVA 2019: Automated Technology for Verification and Analysis. Vol. 11781. p. 81-97

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Reinforcement learning
Teaching
Controllers
Cyber Physical System
2014
214 Downloads (Pure)

Model Checking Process Algebra of Communicating Resources for Real-time Systems

Boudjadar, J., Kim, J. H., Larsen, K. G. & Nyman, U., 2014, Proceedings of ECRTS 2014. IEEE Press, p. 51-60 (Euromicro Conference on Real-Time Systems. Proceedings).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
File
2015
1 Citation (Scopus)

Concurrent weighted logic

Xue, B., Larsen, K. G. & Mardare, R. I., 2015, In : Journal of Logical and Algebraic Methods in Programming. 84, 6, p. 884–897

Research output: Contribution to journalJournal articleResearchpeer-review

Transition Systems
Labels
Concurrent
Synchronization
Logic
2016

An Automata-Based Approach to Trace Partitioned Abstract Interpretation

Olesen, M. C., Hansen, R. R. & Larsen, K. G., 2016, Semantics, Logics and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. Springer, p. 88-110 (Lecture Notes in Computer Science, Vol. 9560).

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

2011
8 Citations (Scopus)

Application of Model-Checking Technology to Controller Synthesis

David, A., Grunnet, J. D., Jessen, J. J., Larsen, K. G. & Rasmussen, J. I., 2011, In : Lecture Notes in Computer Science. 6957, p. 336-351 16 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Model checking
Model Checking
Synthesis
Game
Controller
2015
9 Citations (Scopus)

A Score Function for Optimizing the Cycle-Life of Battery-Powered Embedded Systems

Wognsen, E. R., Haverkort, B., Jongerden, M., Hansen, R. R. & Larsen, K. G., 22 Aug 2015, Formal Modeling and Analysis of Timed Systems: 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings. Springer, p. 305-320 (Lecture Notes in Computer Science, Vol. 9268).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2019

Partial order reduction for reachability games

Bønneland, F. M., Jensen, P. G., Larsen, K. G., Muñiz, M. & Srba, J., Aug 2019, 30th International Conference on Concurrency Theory, CONCUR 2019. Fokkink, W. & van Glabbeek, R. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 140. 23. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 140).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Model checking
Petri nets
2011
15 Citations (Scopus)

Timed Automata Can Always Be Made Implementable

Bouyer, P., Larsen, K. G., Markey, N., Sankur, O. & Thrane, C., 1 Jan 2011, In : Lecture Notes in Computer Science. 6901 LNCS, p. 76-91 16 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Timed Automata
Semantics
Clocks
Synchrony
Timing
2016
1 Citation (Scopus)

Formal modelling and analysis of Bitflips in ARM assembly code

Hansen, R. R., Larsen, K. G., Olesen, M. C. & Wognsen, E. R., 27 Jun 2016, In : Information Systems Frontiers. 18, 5, p. 909–925 17 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

2012
9 Citations (Scopus)

State-of-the-art Tools and Techniques for Quantitative Modeling and Analysis of Embedded Systems

Bozga, M., David, A., Hartmanns, A., Larsen, K. G., Legay, A. & Tretmans, J., 2012, In : A C M / I E E E Design Automation Conference. Proceedings. p. 370-375

Research output: Contribution to journalConference article in JournalResearchpeer-review

Embedded systems
Testing
2017

Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday

Aceto, L. (ed.), Bacci, G. (ed.), Bacci, G. (ed.), Ingolfsdottir, A. (ed.), Larsen, K. G. (ed.), Legay, A. (ed.) & Mardare, R. I. (ed.), 2017, Springer. 1 p. (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues, Vol. 10460).

Research output: Book/ReportAnthologyResearchpeer-review

2015
26 Downloads (Pure)

Parametric Verification of Weighted Systems

Christoffersen, P., Hansen, M., Mariegaard, A., Ringsmose, J. T., Larsen, K. G. & Mardare, R. I., 2015, In : Open Access Series in Informatics. 44, p. 77-90

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
File
Model checking
Linear equations
Linear systems
Mathematical operators
Semantics
2017

Uppaal Stratego for Intelligent Traffic Lights

Eriksen, A. B., Huang, C., Kildebogaard, J., Lahrmann, H. S., Larsen, K. G., Muniz, M. & Taankvist, J. H., 2017, 12th ITS European Congress: Strasbourg, France, 19-22 June 2017. ERTICO - ITS Europe, 10 p. SP0878

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Telecommunication traffic
Controllers
Radar
Cruise control
Information use
2015
19 Citations (Scopus)

Language Emptiness of Continuous-Time Parametric Timed Automata

Benes, N., Bezdek, P., Larsen, K. G. & Srba, J., 2015, Automata, Languages, and Programming: 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II. Halldórsson, M. M., Iwama, K., Kobayashi, N. & Speckmann, B. (eds.). Springer, p. 69-81 12 p. (Lecture Notes in Computer Science; No. 9135).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Clocks
Computability and decidability
Semantics
2012
5 Citations (Scopus)

Statistical Model Checking, Refinement Checking, Optimization, … for Stochastic Hybrid Systems

Larsen, K. G., 2012, Formal Modeling and Analysis of Timed Systems: 10th International Conference, FORMATS 2012, London, UK, September 18-20, 2012. Proceedings. Springer, Vol. 7595. p. 7-10 (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2015
15 Citations (Scopus)

CAAL: Concurrency Workbench, Aalborg Edition

Reimer Andersen, J., Andersen, N., Enevoldsen, S., Munk Hansen, M., Larsen, K. G., Reedtz Olesen, S., Srba, J. & Wortmann, J. K., 2015, Theoretical Aspects of Computing - ICTAC 2015: 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings. Leucker, M., Rueda, C. & Valencia, F. D. (eds.). Netherlands: Springer, p. 573-582 10 p. (Lecture Notes in Computer Science; No. 9399).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

modeling
simulation
analysis
2012
4 Citations (Scopus)
330 Downloads (Pure)

A Modal Specification Theory for Components with Data

Bauer, S. S., Larsen, K. G., Legay, A., Nyman, U. & Wasowski, A., 2012, Formal Aspects of Component Software: 8th International Symposium, FACS 2011, Oslo, Norway, September 14-16, 2011, Revised Selected Papers. Springer Publishing Company, Vol. 7253. (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
File
2014
2 Citations (Scopus)

Parametric and Quantitative Extensions of Modal Transition Systems

Fahrenberg, U., Larsen, K. G., Legay, A. & Traonouez, L-M., 14 Feb 2014, From Programs to Systems.: The Systems perspective in Computing. Bensalem, S., Lakhneck, Y. & Legay, A. (eds.). Springer, Vol. 8415. p. 84-97 (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2016

Automatic Verification, Performance Analysis, Synthesis and Optimization of Timed Systems

Larsen, K. G., 2016, PROCEEDINGS, 23rd International Symposium on Temporal Representation and Reasoning: TIME 2016. IEEE, 1 p.

Research output: Contribution to book/anthology/report/conference proceedingConference abstract in proceedingResearchpeer-review

2018
2 Citations (Scopus)

Analytical Solution for Long Battery Lifetime Prediction in Nonadaptive Systems

Ivanov, D., Larsen, K. G., Schupp, S. & Srba, J., 2018, Quantitative Evaluation of Systems: 15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018, Proceedings. McIver, A. & Horvath, A. (eds.). Springer, p. 173-189 17 p. (Lecture Notes in Computer Science, Vol. 11024).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Hybrid systems
Extrapolation
Statistical methods
Differential equations
Sensors
2013

Preface

Larsen, K. G., Legay, A. & Nyman, U., 3 Nov 2013, Proceedings 1st Workshop on Advances in Systems of Systems. Electronic Proceedings in Theoretical Computer Science, Vol. 133. p. 1-1 (Electronic Proceedings in Theoretical Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingPreface/Introduction/postscriptResearch

1 Citation (Scopus)

Stuttering for Abstract Probabilistic Automata

Delahaye, B., Larsen, K. G. & Legay, A., 2013, Logical Foundations of Computer Science: International Symposium, LFCS 2013, San Diego, CA, USA, January 6-8, 2013. Proceedings. Springer Publishing Company, Vol. 7734. p. 149-163 (Lecture Notes in Computer Science, Vol. 7734).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2017
8 Citations (Scopus)

Mutation-Based Test-Case Generation with Ecdar

Larsen, K. G., Lorber, F., Nielsen, B. & Nyman, U. M., 13 Apr 2017, Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2017. IEEE, p. 319-328 10 p. 7899077

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Testing
Specifications
Alarm systems
Railroad cars
2016
22 Citations (Scopus)

Online and Compositional Learning of Controllers with Application to Floor Heating

Larsen, K. G., Mikučionis, M., Muniz, M., Srba, J. & Taankvist, J. H., 2016, Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016. Springer, p. 244-259 15 p. (Lecture Notes in Computer Science, Vol. 9636).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Heating
Controllers
Analog to digital conversion
Concrete construction
Learning systems
2015
326 Downloads (Pure)

Co-Simulation of Hybrid Systems with SpaceEx and Uppaal

Bogomolov, S., Greitschus, M., Jensen, P. G., Larsen, K. G., Mikučionis, M., Strump, T. & Tripakis, S., 2015, 11th International Modelica Conference Proceedings. Linköping University Electronic Press, p. 159-169 17. (Linköping Electronic Conference Proceedings; No. 118).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
File
Hybrid systems
Model checking
Engines
Heating
Composite materials
2011

Distributed Parametric and Statistical Model Checking

Bulychev, P. E., David, A., Larsen, K. G., Mikucionis, M. & Legay, A., 2011, In : Electronic Proceedings in Theoretical Computer Science. 72, p. 30-42 13 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

2013
14 Citations (Scopus)

Weighted modal transition systems

Bauer, S., Fahrenberg, U., Juhl, L., Legay, A., Larsen, K. G. & Thrane, C., 2013, In : Formal Methods in System Design. 42, 2, p. 193-220

Research output: Contribution to journalJournal articleResearchpeer-review