Distributed, Embedded and Intelligent Systems

  • Selma Lagerlöfs Vej 300, Cassiopeia

    9220 Aalborg

    Denmark

Research Output 1989 2020

2012

A Metric Analogue of Stone Duality for Markov Processes

Larsen, K. G., Mardare, R. I. & Panangaden, P., 2012.

Research output: Contribution to conference without publisher/journalConference abstract for conferenceResearchpeer-review

4 Citations (Scopus)
345 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
29 Citations (Scopus)

An Evaluation Framework for Energy Aware Buildings using Statistical Model Checking

David, A., Du, D., Larsen, K. G., Mikučionis, M. & Skou, A., Dec 2012, In : Science in China. Series F: Information Sciences. 55, 12, p. 2694-2707 14 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Model checking
Hybrid systems
Specifications
Statistical Models
Cyber Physical System
1 Downloads (Pure)

A Secure Relay Protocol for Door Access Control

Wognsen, E. R., Karlsen, H. S., Calverley, M., Follin, M., Thomsen, B. & Hüttel, H., Nov 2012, Proceedings of the XII Brazilian Symposium on Information and Computer System Security: SBSeg 2012. Sociedade Brasileira de Computação (ed.). Porto Alegre, Brasilien: SBC - Sociedade Brasileira de Computação, p. 196-209 14 p. (Anais do SBSeg).

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

32 Citations (Scopus)

Automata Learning through Counterexample Guided Abstraction Refinement

Aarts, F., Heidarian, F., Kuppens, H., Olsen, P. & Vaandrager, F., 2012, FM 2012: Formal Methods : 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. Springer, Vol. 7436. p. 10-27 18 p. (Lecture Notes in Computer Science, Vol. 7436).

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

Finite automata
Biometrics
Concretes
Network protocols
23 Citations (Scopus)

Behavioural modelling and verification of real-time software product lines

Cordy, M., Schobbens, P-Y., Heymans, P. & Legay, A., 1 Jan 2012, SPLC '12 Proceedings of the 16th International Software Product Line Conference. Association for Computing Machinery, Vol. 1. p. 66-75 10 p. (ACM International Conference Proceeding Series (ICPS)).

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

Model checking
Formal methods
Software engineering
26 Citations (Scopus)

Checking and Distributing Statistical Model Checking

Bulychev, P. E., David, A., Larsen, K. G., Legay, A., Mikučionis, M. & Poulsen, D. B., 3 Apr 2012, NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. Goodloe, A. E. & Person, S. (eds.). Springer, Vol. 7226. p. 449-463 15 p. (Lecture Notes in Computer Science, Vol. 7226).

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

Code-level timing analysis of embedded software: emsoft'12 invited talk session outline

Falk, H., Hammong, K., Larsen, K. G., Lisper, B. & Petters, S. M., 2012, EMSOFT '12 Proceedings of the tenth ACM international conference on Embedded software . Association for Computing Machinery, p. 163-164 2 p.

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

Combining Epistemic Logic and Hennessy-Milner Logic

Knight, S., Mardare, R. I. & Panangaden, P., 2012, Logic and Program Semantics: Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday. Constable, R. L. & Silva, A. (eds.). Springer Science+Business Media, Vol. 7230. p. 219-243 (Lecture Notes in Computer Science).

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

39 Citations (Scopus)

Compositional Safety Analysis using Barrier Certificates

Sloth, C., Pappas, G. J. & Wisniewski, R., 2012, HSCC '12 Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control. New York: Association for Computing Machinery, p. 15-24 9 p.

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

Plant shutdowns
Wind turbines
Dynamical systems
Chemical analysis
13 Citations (Scopus)
290 Downloads (Pure)

Compositional verification of real-time systems using Ecdar

David, A., Larsen, K. G., Møller, M. H., Nyman, U., Ravn, A. P., Skou, A., Legay, A. & Wasowski, A., 15 Jun 2012, In : International Journal on Software Tools for Technology Transfer. 14, 6, p. 703-720 18 p.

Research output: Contribution to journalJournal articleResearchpeer-review

File
Real time systems
Specifications
Network protocols

Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach

Bulychev, P. E., David, A., Larsen, K. G., Legay, A. & Mikučionis, M., 20 Feb 2012, Proceedings Second International Workshop on Interactions, Games and Protocols. Reich, J. & Finkbeiner, B. (eds.). Tallin, Estonia, p. 1-14 14 p. (Electronic Proceedings in Theoretical Computer Science, Vol. 78).

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

Carrier sense multiple access
Wireless ad hoc networks
Model checking
Wireless networks
Network protocols
10 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

10 Citations (Scopus)

Continuous Markovian Logics: Axiomatization and Quantified Metatheory

Mardare, R. I., Cardelli, L. & Larsen, K. G., 29 Nov 2012, In : Logical Methods in Computer Science. 8, 4, p. 1-29

Research output: Contribution to journalJournal articleResearchpeer-review

Axiomatization
Markov processes
Logic
Markov Process
Random variables

Controllers with Minimal Observation Power (Application to Timed Systems)

Bulychev, P., Cassez, F., David, A., Larsen, K. G., Raskin, J-F. & Reynier, P-A., Oct 2012, Automated Technology for Verification and Analysis: 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings. Springer, Vol. 7561. p. 223-237 15 p. (Lecture Notes in Computer Science, Vol. 7561).

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

Set theory
Cost functions
Controllers
Costs

D2.3 - ENCOURAGE platform reference architecture

Ferreira, L. L., Pinho, L. M., Albano, M., Ramiro, M., Faria, E., Ferreira, R., Gaylard, E., Roarke, E., Dueñas, L. P., Cano Gimeno, N., Le Guilly, T., Madsen, P. P., Jorquera, D., Lux, D. & Los, M., 10 May 2012, 101 p.

Research output: Book/ReportReportResearchpeer-review

Decidability of Modular Logics for Concurrency

Mardare, R. I., 2012, Perspectives of Systems Informatics: 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27-July 1, 2011, Revised Selected Papers. Berlin: Springer, Vol. 7162. p. 274-288 (Lecture Notes in Computer Science, Vol. 7162).

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

19 Citations (Scopus)

Derivation and validation of a coal mill model for control

Niemczyk, P., Bendtsen, J. D., Ravn, A. P., Andersen, P. & Pedersen, T. S., May 2012, In : Control Engineering Practice. 20, 5, p. 519-530 12 p.

Research output: Contribution to journalJournal articleResearchpeer-review

10 Citations (Scopus)

Dual-Priced Modal Transition Systems with Time Durations

Beneš, N., Kretínsky, J., Larsen, K. G., Møller, M. H. & Srba, J., 2012, Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics: 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings . Netherlands: Springer, Vol. LNCS 7180. p. 122-137 15 p. (Lecture Notes in Computer Science, Vol. 7180).

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

Hardware
Costs
Specifications
7 Citations (Scopus)

EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems

Beneš, N., Křetínský, J., Larsen, K. G. & Srba, J., 2012, In : Information and Computation. 218, 1, p. 54-68 15 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Transition Systems
Completeness
Refinement
Computational complexity
Exponential time
19 Citations (Scopus)

Extending Modal Transition Systems with Structured Labels

Bauer, S. S., Juhl, L., Larsen, K. G., Legay, A. & Srba, J., 8 May 2012, In : Mathematical Structures in Computer Science. 22, 4, p. 581-617 37 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Transition Systems
Labels
Refinement
Specification
Parallel Composition

Formal Analyses of Web Service Protocols

Vighio, S., Mar 2012, Aalborg. 224 p. (Ph.D. thesis; No. 70).

Research output: Book/ReportPh.D. thesisResearch

4 Citations (Scopus)

Formal Analysis of Privacy for Anonymous Location Based Services

Dahl, M., Delaune, S. & Steel, G., 2012, Theory of Security and Applications: Joint Workshop, TOSCA 2011, Saarbrücken, Germany, March 31 - April 1, 2011, Revised Selected Papers. Mödersheim, S. & Palamidessi, C. (eds.). Springer Publishing Company, p. 98-112 (Lecture Notes in Computer Science, Vol. 6993).

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

589 Downloads (Pure)

Formal Verification of Continuous Systems

Sloth, C., 2012, 225 p.

Research output: Book/ReportPh.D. thesisResearch

Open Access
File
Dynamical systems
Specifications
Formal verification
Large scale systems
Control systems
14 Citations (Scopus)

General quantitative specification theories with modalities

Bauer, S. S., Fahrenberg, U., Legay, A. & Thrane, C., 2012, Computer Science – Theory and Applications: 7th International Computer Science Symposium in Russia, CSR 2012, Nizhny Novgorod, Russia, July 3-7, 2012. Proceedings. Hirsch, E. A., Karhumäki, J., Lepistö, A. & Prilutskii, M. (eds.). Springer Publishing Company, p. 18-30 13 p. (Lecture Notes in Computer Science, Vol. 7353).

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

Modality
Specification
System Design
Refinement
Generalise
524 Downloads (Pure)

Java for Cost Effective Embedded Real-Time Software

Korsholm, S., Aug 2012, Department of Computer Science, Aalborg University. 75 p.

Research output: Book/ReportPh.D. thesisResearch

File

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
10 Citations (Scopus)
339 Downloads (Pure)

Learning Markov models for stationary system behaviors

Chen, Y., Mao, H., Jaeger, M., Nielsen, T. D., Larsen, K. G. & Nielsen, B., 2012, NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. Goodloe, A. E. & Person, S. (eds.). Springer, p. 216-230 15 p. (Lecture Notes in Computer Science, Vol. 7226).

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

File
Embedded systems
Markov processes
Learning systems
Hardware
Experiments
10 Citations (Scopus)

Lower-Bound Constrained Runs in Weighted Timed Automata

Bouyer, P., Larsen, K. G. & Markey, N., 2012, Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012. London: IEEE Computer Society Press, p. 128-137

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

7 Citations (Scopus)

mctau: Bridging the Gap between Modest and UPPAAL

Bogdoll, J., David, A., Harmanns, A. & Hermanns, H., 2012, Model Checking Software: 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings. Donaldson, A. & Parker, D. (eds.). Berlin: Springer, Vol. 7385. p. 227-233 7 p. (Lecture Notes in Computer Science (LNCS), Vol. 7385).

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

Semantics
Modeling languages
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

14 Citations (Scopus)

Modal Transition Systems with Weight Intervals

Juhl, L., Larsen, K. G. & Srba, J., May 2012, In : Journal of Logic and Algebraic Programming. 81, 4, p. 408-421 14 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Transition Systems
Specifications
Interval
Refinement
Specification
22 Citations (Scopus)

Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic

Bulychev, P., David, A., Larsen, K. G., Legay, A., Guangyuan, L., Poulsen, D. B. & Stainer, A., 2012, Logic for Programming, Artificial Intelligence, and Reasoning: 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings. Berlin: Springer, Vol. 7180. p. 168-182 (Lecture Notes in Computer Science, Vol. 7180).

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

Temporal logic
Model checking
Semantics
Statistical Models
67 Citations (Scopus)
465 Downloads (Pure)

Moving from Specifications to Contracts in Component-based Design

Bauer, S., David, A., Hennicker, R., Larsen, K. G., Legay, A., Nyman, U. & Wasowski, A., 2012, Fundamental Approaches to Software Engineering 15th International Conference, FASE 2012: 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Springer, Vol. 7212. p. 43-58 15 p. (Lecture Notes in Computer Science, Vol. 7212).

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

Open Access
File
13 Citations (Scopus)

Multi-core reachability for timed automata

Dalsgaard, A. E., Laarman, A., Larsen, K. G., Olesen, M. C. & Van De Pol, J., 2012, Formal Modeling and Analysis of Timed Systems: 10th International Conference, FORMATS 2012, London, UK, September 18-20, 2012. Proceedings. Jurdzinski, M. & Nickovic, D. (eds.). Springer Publishing Company, p. 91-106 16 p. (Lecture Notes in Computer Science, Vol. 7595).

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

Model checking
Parallel algorithms
Data structures
Scalability
Hardware
9 Citations (Scopus)

Nash Equilibria in Concurrent Priced Games

Klimos, M., Larsen, K. G., Stefanak, F. & Thaarup, J., 2012, Language and Automata Theory and Applications: 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012. Proceedings. Berlin: Springer, Vol. 7183. p. 363-376 (Lecture Notes in Computer Science, Vol. 7183).

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

2 Citations (Scopus)

New Results for Constraint Markov Chains

Delahaye, B., Larsen, K. G., Legay, A., Pedersen, M. L. & Wasowski, A., 2012, In : Performance Evaluation. 69, 7-8, p. 379-401

Research output: Contribution to journalJournal articleResearchpeer-review

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

21 Citations (Scopus)

Passive Fault-tolerant Control of Discrete-time Piecewise Affine Systems against Actuator Faults

Tabatabaeipour, S. M., Izadi-Zamanabadi, R., Bak, T. & Ravn, A. P., Nov 2012, In : International Journal of Systems Science. 43, 11, p. 1985-1997 13 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Piecewise Affine Systems
Passive Control
Fault-tolerant Control
Linear matrix inequalities
Matrix Inequality
7 Citations (Scopus)

Private memory allocation analysis for safety-critical java

Dalsgaard, A. E., Hansen, R. R. & Schoeberl, M., 2012, JTRES '12 Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems. Association for Computing Machinery, p. 9-17 9 p. (Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems).

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

Storage allocation (computer)
Data storage equipment

Probabilistic logic and the metric space of logical formulas

Mardare, R. I., Sep 2012, In : Bulletin of Symbolic Logic. 18, 3, p. 455

Research output: Contribution to journalConference abstract in journalResearchpeer-review

Probabilistic Logic
Metric space
Logic
Meeting Report
Colloquium
655 Downloads (Pure)

Proceedings of the ICTSS 2012 Ph.D. Workshop

Weise, C. (ed.) & Nielsen, B. (ed.), 19 Nov 2012, Aalborg.

Research output: Book/ReportAnthologyResearchpeer-review

Open Access
File
188 Downloads (Pure)

Proceedings of the ICTSS 2012 PhD Workshop - Preface

Nielsen, B. & Weise, C., 19 Nov 2012, Proceedings of the ICTSS 2012 PhD Workshop - Preface. Aalborg ed. Department of Computer Science, Aalborg University, Vol. 12-201. p. 1

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

Open Access
File

Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software

Pace, G. (ed.) & Ravn, A. P. (ed.), 8 Sep 2012, In : Electronic Notes in Theoretical Computer Science. 94

Research output: Contribution to journalJournal articleResearchpeer-review

Quantitative Modeling and Analysis

Katoen, J-P. & Larsen, K. G., 2012, Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies: 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part II. Berlin: Springer, Vol. 7610. p. 290-292 (Lecture Notes in Computer Science, Vol. 7610).

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

10 Citations (Scopus)
377 Downloads (Pure)

Reachability analysis for timed automata using max-plus algebra

Lu, Q., Madsen, M., Milata, M., Ravn, S., Fahrenberg, U. & Larsen, K. G., 2012, In : Journal of Logic and Algebraic Programming. 81, 3, p. 298-313

Research output: Contribution to journalJournal articleResearchpeer-review

File
Max-plus Algebra
Reachability Analysis
Timed Automata
Polyhedron
Algebra
22 Citations (Scopus)

Runtime Verification of Biological Systems

David, A., Larsen, K. G., Legay, A., Mikucionis, M., Poulsen, D. B. & Sedwards, S., 2012, Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change: 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I. Berlin: Springer, Vol. 7609. p. 388-404 17 p. (Lecture Notes in Computer Science, Vol. 7609).

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

18 Citations (Scopus)

Safety-critical Java for low-end embedded platforms

Søndergaard, H., Korsholm, S. E. & Ravn, A. P., 2012, Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems . Association for Computing Machinery, p. 44-53 (ACM International Conference Proceeding Series (ICPS)).

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