Distributed, Embedded and Intelligent Systems

  • Selma Lagerlöfs Vej 300, Cassiopeia

    9220 Aalborg

    Denmark

Research Output 1989 2020

Filter
Conference article in Journal
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
2018
1 Citation (Scopus)
82 Downloads (Pure)

Complete Axiomatization for the Total Variation Distance of Markov Chains

Bacci, G., Bacci, G., Larsen, K. G. & Mardare, R., 16 Apr 2018, In : Electronic Notes in Theoretical Computer Science. 336, p. 27-39 13 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
File
Total Variation Distance
Axiomatization
Markov processes
Markov chain
Deduction

Control Synthesis for Stochastic Switched Systems using the Tamed Euler Method

Coënt, A. L., Fribourg, L. & Vacher, J., 1 Jan 2018, In : IFAC-PapersOnLine. 51, 16, p. 259-264 6 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

113 Downloads (Pure)

Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar

Gundersen, T. R., Lorber, F., Nyman, U. & Ovesen, C., 7 Sep 2018, In : Electronic Proceedings in Theoretical Computer Science. 277, p. 147-160 14 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
File
Real time systems
Model checking
Testing
2017
3 Citations (Scopus)

A delay-robust touristic plan recommendation using real-world public transportation information

Ayala, V. A. A., Alzogbi, A., Gülsen, K. C., Färber, M., Muñiz, M. & Lausen, G., 1 Jan 2017, In : CEUR Workshop Proceedings. 1906, p. 9-17 9 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Recommender systems
Experiments
18 Citations (Scopus)

Compositional bisimulation metric reasoning with Probabilistic Process Calculi

Gebler, D., Larsen, K. G. & Tini, S., 2017, In : Logical Methods in Computer Science. 12, 4

Research output: Contribution to journalConference article in JournalResearch

Open Access
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
27 Downloads (Pure)
Open Access
File
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

2015
28 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
2014
1 Citation (Scopus)

Adaptive Task Automata with Earliest-Deadline-First Scheduling

Hatvani, L., David, A., Seceleanu, C. & Pettersson, P., 2014, In : Electronic Communications of the EASST. 70, p. 1-15 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
2 Citations (Scopus)
466 Downloads (Pure)

Coccinelle: Tool support for automated CERT C Secure Coding Standard certification

Olesen, M. C., Hansen, R. R., Lawall, J. L. & Palix, N. J-M., Oct 2014, In : Science of Computer Programming. 91, Part B, p. 141-160

Research output: Contribution to journalConference article in JournalResearchpeer-review

File
10 Citations (Scopus)

Lower-bound-constrained runs in weighted timed automata

Bouyer, P., Larsen, K. G. & Markey, N., 19 May 2014, In : Performance Evaluation. 73, p. 91-109 73.

Research output: Contribution to journalConference article in JournalResearchpeer-review

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
8 Citations (Scopus)

Robust synthesis for real-time systems

Larsen, K. G., Legay, A., Traonouez, L-M. & Wasowski, A., 2 Jan 2014, In : Theoretical Computer Science. 515, p. 92-122

Research output: Contribution to journalConference article in JournalResearchpeer-review

Statistical model checking of dynamic networks of stochastic hybrid automata

David, A., Larsen, K. G., Legay, A. & Poulsen, D. B., 2014, In : Electronic Communications of the EASST. 66, 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
1 Citation (Scopus)

Stuttering for abstract probabilistic automata

Delahaye, B., Larsen, K. G. & Legay, A., 2014, In : Journal of Logic and Algebraic Programming. 83, 1, p. 1-19

Research output: Contribution to journalConference article in JournalResearchpeer-review

2013

Externalizing Behaviour for Analysing System Models

Ivanova, M. G., Probst, C. W., Hansen, R. R. & Kammüller, F., Nov 2013, In : Journal of Internet Services and Information Security. 3, 3/4, p. 52-62

Research output: Contribution to journalConference article in JournalResearchpeer-review

3 Citations (Scopus)

Reachability-based Impact as a Measrue for Insiderness

Probst, C. W. & Hansen, R. R., Dec 2013, In : Journal of Wireless Mobile Networks, Ubiquitous Computing and Dependable Applications. 4, 4, p. 38-48 11 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

2012

A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets

David, A., Jacobsen, L., Jacobsen, M. & Srba, J., 2012, In : Electronic Proceedings in Theoretical Computer Science. 102, p. 125-140 16 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Petri nets
Extrapolation

Learning Markov Decision Processes for Model Checking

Mao, H., Chen, Y., Jaeger, M., Nielsen, T. D., Larsen, K. G. & Nielsen, B., 2012, In : Electronic Proceedings in Theoretical Computer Science. 103, p. 49-63

Research output: Contribution to journalConference article in JournalResearchpeer-review

Model checking
Temporal logic
Finite automata
Learning algorithms
Learning systems
2 Citations (Scopus)

MDM: A Mode Diagram Modeling Framework

Wang, Z., Pu, G., Li, J., He, J., Qin, S., Larsen, K. G., Madsen, J. & Gu, B., 2012, In : Electronic Proceedings in Theoretical Computer Science. 105, p. 135-149

Research output: Contribution to journalConference article in JournalResearchpeer-review

11 Citations (Scopus)

On the Existence of Compositional Barrier Certificates

Sloth, C., Wisniewski, R. & Pappas, G. J., 2012, In : I E E E Conference on Decision and Control. Proceedings. p. 4580-4585 6 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Certificate
Barrier Function
Safety Analysis
Counterexample
Subsystem

Parameterized Metatheory for Continuous Markovian Logic

Larsen, K. G., Mardare, R. I. & Thrane, C., 2012, In : Electronic Proceedings in Theoretical Computer Science. 103, p. 33-47

Research output: Contribution to journalConference article in JournalResearchpeer-review

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

Time-Darts: A Data Structure for Verification of Closed Timed Automata

Jørgensen, K. Y., Larsen, K. G. & Srba, J., 2012, In : Electronic Proceedings in Theoretical Computer Science. 102, p. 141-155 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Data structures
Clocks
Model checking
Petri nets
Explosions
66 Citations (Scopus)

UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

Bulychev, P., David, A., Larsen, K. G., Mikučionis, M., Poulsen, D. B., Legay, A. & Wang, Z., 2012, In : Electronic Proceedings in Theoretical Computer Science. 85, p. 1-16 17 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Model checking
Probability distributions
Semantics
Statistical Models
2011
33 Citations (Scopus)

Abstract Probabilistic Automata

Delahaye, B., Katoen, J-P., Larsen, K. G., Legay, A., Pedersen, M. L., Sher, F. & Wasowski, A., 2011, In : Lecture Notes in Computer Science. 6538, p. 324-339

Research output: Contribution to journalConference article in JournalResearchpeer-review

1 Citation (Scopus)
297 Downloads (Pure)

Algorithmic Approach to Abstracting Linear Systems by Timed Automata

Sloth, C. & Wisniewski, R., 2011, In : I F A C Workshop Series. p. 4546-4551 6 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
File
Lyapunov functions
Linear systems
Dynamical systems
Trajectories
29 Citations (Scopus)

An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres

Hilscher, M., Linker, S., Olderog, E-R. & Ravn, A. P., 2011, In : Lecture Notes in Computer Science. 6991, p. 404-419 16 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Railroad cars
Safety
Traffic
Controller
Model
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
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

Distances for Weighted Transition Systems: Games and Properties

Fahrenberg, U., Thrane, C. R. & Larsen, K. G., 2011, In : Electronic Proceedings in Theoretical Computer Science. 57, p. 134-147 14 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

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

50 Citations (Scopus)

Energy Games in Multiweighted Automata

Fahrenberg, U., Juhl, L., Larsen, K. G. & Srba, J., 1 Jan 2011, In : Lecture Notes in Computer Science. 6916, p. 95-115 21 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Computability and decidability
Finite automata
Petri nets
Automata
Game
4 Citations (Scopus)

Model-based testing of industrial transformational systems

Olsen, P., Foederer, J. & Tretmans, J., 2011, In : Lecture Notes in Computer Science. 7019, p. 131-145 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Model-based Testing
Output
Testing
Test Set
Large scale systems
14 Citations (Scopus)

Modelling and Verification of Web Services Business Activity Protocol

Ravn, A. P., Srba, J. & Vighio, S., 2011, In : Lecture Notes in Computer Science. 6605, p. 357--371 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Web services
Web Services
Network protocols
Modeling
Industry
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
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
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

8 Citations (Scopus)
381 Downloads (Pure)

Opaal: A Lattice Model Checker

Dalsgaard, A. E., Hansen, R. R., Jørgensen, K. Y., Larsen, K. G., Olesen, M. C., Olsen, P. & Srba, J., 2011, In : Lecture Notes in Computer Science. 6617, p. 487-493 5 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
File
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
18 Citations (Scopus)

Quantitative Refinement for Weighted Modal Transition Systems

Bauer, S. S., Fahrenberg, U., Juhl, L., Larsen, K. G., Legay, A. & Thrane, C., 1 Jan 2011, In : Lecture Notes in Computer Science. 6907 LNCS, p. 60-71 12 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Transition Systems
Refinement
Specification
Specifications
Software System
13 Citations (Scopus)

Robust specification of real time components

Larsen, K. G., Legay, A., Traonouez, L-M. & Wasowski, A., 1 Jan 2011, In : Lecture Notes in Computer Science. 6919 LNCS, p. 129-144 16 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Specification
Specifications
Robustness
Parallel Composition
Timed Automata
86 Citations (Scopus)

Statistical Model Checking for Networks of Priced Timed Automata

David, A., Larsen, K. G., Mikucionis, M., Poulsen, D. B., Vliet, J. V., Legay, A. & Wang, Z., 1 Jan 2011, In : Lecture Notes in Computer Science. 6919 LNCS, p. 80-96 17 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Timed Automata
Model checking
Model Checking
Statistical Model
Semantics
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
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
1 Citation (Scopus)

Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols

Dahl, M., Kobayashi, N., Sun, Y. & Hüttel, H., 2011, In : Lecture Notes in Computer Science. 6996, p. 75-89 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

10 Citations (Scopus)

Typed ψ-calculi

Hüttel, H., 2011, In : Lecture Notes in Computer Science. 6901, p. 265-279 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

28 Citations (Scopus)

Verification of Timed-Arc Petri Nets

Jacobsen, L., Jacobsen, M., Møller, M. H. & Srba, J., 2011, In : Lecture Notes in Computer Science. 6543, p. 46-72 26 p.

Research output: Contribution to journalConference article in JournalResearch

Petri nets
Petri Nets
Arc of a curve
Automatic Verification
Timed Automata