Scheduling with timed automata

DOI10.1016/j.tcs.2005.11.018zbMath1088.68023OpenAlexW1987234253MaRDI QIDQ2368955

Eugene Asarin, Oded Maler, Yasmina Abdeddaïm

Publication date: 28 April 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.11.018

zbMATH Keywords

SchedulingTimed automataVerification and synthesis

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20)

Related Items (22)

Performance Evaluation of Schedulers in a Probabilistic Setting ⋮ Model Checking Real-Time Systems ⋮ Solving the time varying postman problems with timed automata ⋮ Computational techniques for reachability analysis of Max-Plus-Linear systems ⋮ A study on shuffle, stopwatches and independently evolving clocks ⋮ A multi-objective approach for manufacturing systems with multiple production routes based on supervisory control theory and heuristic algorithms ⋮ Robust reachability in timed automata and games: a game-based approach ⋮ Parameter synthesis for hierarchical concurrent real-time systems ⋮ Timed discrete event control of parallel production lines with continuous outputs ⋮ Models and formal verification of multiprocessor system-on-chips ⋮ The Unmet Challenge of Timed Systems ⋮ Decomposition of timed automata for solving scheduling problems ⋮ A menagerie of timed automata ⋮ Discount-Optimal Infinite Runs in Priced Timed Automata ⋮ Survey on Directed Model Checking ⋮ Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking ⋮ Supervisor synthesis and throughput optimization of partially-controllable manufacturing systems ⋮ Optimal work-conserving scheduler synthesis for real-time sporadic tasks using supervisory control of timed discrete-event systems ⋮ Model Checking Logic WCTL with Multi Constrained Modalities on One Clock Priced Timed Automata ⋮ Using formal verification to evaluate the execution time of Spark applications ⋮ Model checking for entanglement swapping ⋮ Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints*

Uses Software

• Kronos
• IF-2.0
• Uppaal

Cites Work

• Minimum and maximum delay problems in real-time systems
• Model-checking in dense real-time
• A theory of timed automata
• Symbolic model checking for real-time systems
• Deterministic job-shop scheduling: Past, present and future
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Computing efficient operation schemes for chemical plants in multi-batch mode
• Compositional specification of timed systems
• On the synthesis of discrete controllers for timed systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Scheduling with timed automata