Skip to main navigation Skip to search Skip to main content

Decidable and undecidable problems in schedulability analysis using timed automata

  • Pavel Krčál*
  • , Wang Yi
  • *Corresponding author for this work
  • Uppsala University

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

Abstract

We study schedulability problems of timed systems with nonuniformly recurring computation tasks. Assume a set of real time tasks whose best and worst execution times, and deadlines are known. We use timed automata to describe the arrival patterns (and release times) of tasks. From the literature, it is known that the schedulability problem for a large class of such systems is decidable and can be checked efficiently. In this paper, we provide a summary on what is decidable and what is undecidable in schedulability analysis using timed automata. Our main technical contribution is that the schedulability problem will be undecidable if these three conditions hold: (1) the execution times of tasks are intervals, (2) a task can announce its completion time, and (3) a task can preempt another task. We show that if one of the above three conditions is dropped, the problem will be decidable. Thus our result can be used as an indication in identifying classes of timed systems that can be analysed efficiently.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsKurt Jensen, Andreas Podelski
PublisherSpringer Verlag
Pages236-250
Number of pages15
ISBN (Print)354021299X, 9783540212997
DOIs
StatePublished - 2004
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2988
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Decidable and undecidable problems in schedulability analysis using timed automata'. Together they form a unique fingerprint.

Cite this