A theory of timed automata

From MaRDI portal

Publication:1322162

Jump to:navigation, search

DOI10.1016/0304-3975(94)90010-8zbMath0803.68071OpenAlexW2101508170MaRDI QIDQ1322162

David L. Dill, Rajeev Alur

Publication date: 5 May 1994

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

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90010-8

zbMATH Keywords

verification undecidability timed automata Büchi automata PSPACE-complete behavior of real-time systems deterministic timed Muller automata modeling of time nondeterministic timed automata timed language

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

New Results on Timed Specifications, Performance Evaluation of Schedulers in a Probabilistic Setting, Time-Bounded Verification of CTMCs against Real-Time Specifications, Probabilistic Real-Time Rewrite Theories and Their Expressive Power, Statistical Model Checking for Networks of Priced Timed Automata, Robust Model-Checking of Timed Automata via Pumping in Channel Machines, Thin and Thick Timed Regular Languages, Robust Specification of Real Time Components, Minimum Attention Controller Synthesis for Omega-Regular Objectives, Exact Incremental Analysis of Timed Automata with an SMT-Solver, Event Clock Automata: From Theory to Practice, Composing Stability Proofs for Hybrid Systems, Modeling for Verification, Binary Decision Diagrams, Combining Model Checking and Deduction, Model Checking Real-Time Systems, Verification of Hybrid Systems, Symbolic Model Checking in Non-Boolean Domains, An Abstract Model for Proving Safety of Autonomous Urban Traffic, Weighted Register Automata and Weighted Logic on Data Words, Parametric Deadlock-Freeness Checking Timed Automata, Volume and Entropy of Regular Timed Languages: Discretization Approach, Concavely-Priced Probabilistic Timed Automata, Time-Bounded Verification, Weak Time Petri Nets Strike Back!, Strict Divergence for Probabilistic Timed Automata, Coinduction in Concurrent Timed Systems, Tropical Fourier–Motzkin elimination, with an application to real-time verification, A Logical Characterization of Timed Pushdown Languages, Quantifying Communication in Synchronized Languages, Analyzing Oscillatory Behavior with Formal Methods, Timed Symbolic Dynamics, Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels, Improving Search Order for Reachability Testing in Timed Automata, Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata, Quantitative Attack Tree Analysis via Priced Timed Automata, Fluid Model Checking of Timed Properties, Nested Timed Automata with Frozen Clocks, Verification and Control of Partially Observable Probabilistic Real-Time Systems, Deciding Concurrent Planar Monotonic Linear Hybrid Systems, Bounded Determinization of Timed Automata with Silent Transitions, Logics for Weighted Timed Pushdown Automata, Security of Numerical Sensors in Automata, Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems, Formal Modelling, Analysis and Verification of Hybrid Systems, Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms, Relating timed and register automata, A rewriting framework and logic for activities subject to regulations, Fault-tolerant continuous flow systems modelling, Unnamed Item, Unnamed Item, Unnamed Item, Optimal Reachability in Divergent Weighted Timed Games, Parametric Timed Model Checking for Guaranteeing Timed Opacity, Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata, Efficient CTMC Model Checking of Linear Real-Time Objectives, Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy, An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP, Rigorous Simulation-Based Analysis of Linear Hybrid Systems, Expressiveness of verifiable hierarchical clock systems, Emptiness and Universality Problems in Timed Automata with Positive Frequency, On Reachability for Hybrid Automata over Bounded Time, VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES, THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Methodologies for Specification of Real-Time Systems Using Timed I/O Automata, Well (and Better) Quasi-Ordered Transition Systems, Access Nets: Modeling Access to Physical Spaces, Verification of Timed-Arc Petri Nets, Predicate Abstraction for Dense Real-Time Systems1 1This research was supported by the National Science Foundation under grants CCR-00-82560 and CCR-00-86096 and by NASA Langley Research Center under contract B09060051 and Cooperative Agreement NCC-1-399 with Honeywell Minneapolis. Most of this research has been conducted while the first author was visiting SRI International, July/August 2001., Timed Automata Can Always Be Made Implementable, Coarse Abstractions Make Zeno Behaviours Difficult to Detect, Fixed-Delay Events in Generalized Semi-Markov Processes Revisited, Formal Models of Timing Attacks on Web Privacy, Rule Formats for Timed Processes, Translation from timed Petri nets with intervals on transitions to intervals on places (with urgency), Verification of Asynchronous Circuits using Timed Automata, On Improving Backwards Verification of Timed Automata (Extended Abstract), TPAP, Timed Semantics of Message Sequence Charts Based on Timed Automata, Modular Synthesis of Timed Circuits using Partial Orders on LPNs, Parking Can Get You There Faster, Classes of Timed Automata and the Undecidability of Universality, Timed CSP = Closed Timed Automata1, Proving Safety of Traffic Manoeuvres on Country Roads, A modular formal semantics for Ptolemy, Rigorous implementation of real-time systems – from theory to application, Non-Interference Control Synthesis for Security Timed Automata, Recent Advances in Real-Time Maude, Proving Approximate Implementations for Probabilistic I/O Automata, Time Separation of Events: An Inverse Method, Keeping Secrets in Resource Aware Components, Automated formal analysis and verification: an overview, Towards Deriving Test Sequences by Model Checking, Automatic Verification of Combined Specifications: An Overview, On Verification of Linear Occurrence Properties of Real-Time Systems, Modelling and analysing neural networks using a hybrid process algebra, Timed recursive state machines: expressiveness and complexity, Timed hyperproperties, Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey, The complexity of synchronous notions of information flow security, Expected reachability-time games, Adequacy and complete axiomatization for timed modal logic, Spotlight abstraction in model checking real-time task schedulability, On the complexity of timed pattern matching, An integer static analysis for better extrapolation in Uppaal, Tweaking the odds in probabilistic timed automata, \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability, Fast zone-based algorithms for reachability in pushdown timed automata, Molecular computers for molecular robots as hybrid systems, A note on the verification of automata specifications of probabilistic real-time systems, Determinization of timed Petri nets behaviors, Dynamic controllability via timed game automata, Formal assessment of reliability specifications in embedded cyber-physical systems, Models with virtual force carriers in classical particle physics, Better abstractions for timed automata, Quantifying communication in synchronized languages, Rewriting modulo SMT and open system analysis, A new model for model checking: cycle-weighted Kripke structure, Optimal paths in weighted timed automata, Bisimulation on speed: Worst-case efficiency, SetExp: a method of transformation of timed automata into finite state automata, Learning of event-recording automata, Weak bisimulation for probabilistic timed automata, Aspects of availability. Enforcing timed properties to prevent denial of service, A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences, Automata-theoretic decision of timed games, Robust synthesis for real-time systems, Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems, A game-theoretic approach to fault diagnosis and identification of hybrid systems, Similarity in languages and programs, A survey of timed automata for the development of real-time systems, Validation and verification of web services choreographies by using timed automata, General quantitative specification theories with modal transition systems, Combined model checking for temporal, probabilistic, and real-time logics, Low dimensional hybrid systems -- decidable, undecidable, don't know, The sweep-line state space exploration method, Efficiently identifying deterministic real-time automata from labeled data, A Kleene-Schützenberger theorem for weighted timed automata, Scenario-based verification of real-time systems using UPPAAL, Weighted o-minimal hybrid systems, Automata and logics over finitely varying functions, Regular set of representatives for time-constrained MSC graphs, State-based scheduling with tree schedules: analysis and evaluation, Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}, Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets, Reachability analysis for timed automata using max-plus algebra, Interrupt timed automata: verification and expressiveness, Efficient emptiness check for timed Büchi automata, A concurrency-preserving translation from time Petri nets to networks of timed automata, Hardness of preorder checking for basic formalisms, Control: a perspective, Finite-state automata in information technologies, Efficient verification of distributed real-time systems with broadcasting behaviors, Constraint LTL satisfiability checking without automata, A succinct canonical register automaton model, Learning register automata: from languages to program structures, Improving active Mealy machine learning for protocol conformance testing, Robust reachability in timed automata and games: a game-based approach, Supervisory controller design to enforce some basic properties in timed-transition Petri nets using stretching, On regions and zones for event-clock automata, Runtime enforcement of timed properties revisited, Parameter synthesis for hierarchical concurrent real-time systems, Structural transformations for data-enriched real-time systems, Untiming timed languages, Graph-based models for real-time workload: a survey, Applications of an expressive statistical model checking approach to the analysis of genetic circuits, The algorithmic analysis of hybrid systems, Symbolic bisimulations, Finding minimum and maximum termination time of timed automata models with cyclic behaviour, On parametric timed automata and one-counter machines, Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata, Compositional schedulability analysis of real-time actor-based systems, Linear logic as a tool for planning under temporal uncertainty, Model checking weighted integer reset timed automata, A contract-based approach to adaptivity, MSO logics for weighted timed automata, Timed modal logics for real-time systems. Specification, verification and control, Linear reachability problems and minimal solutions to linear Diophantine equation systems, The efficiency of identifying timed automata and the power of clocks, Reachability results for timed automata with unbounded data structures, On the completeness and decidability of duration calculus with iteration, Quantitative analysis of weighted transition systems, On timed alternating simulation for concurrent timed games, Counting and generating permutations in regular classes, A logical characterization of timed regular languages, Robustness of temporal logic specifications for continuous-time signals, Time-budgeting: a component based development methodology for real-time embedded systems, Towards verification of computation orchestration, Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application, Verification of continuous dynamical systems by timed automata, Using formal verification to evaluate the execution time of Spark applications, Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point, Checking timed Büchi automata emptiness efficiently, A supervisory control method for ensuring the conformance of real-time discrete event systems, A tool for deciding the satisfiability of continuous-time metric temporal logic, Configurable verification of timed automata with discrete variables, Automatic synthesis of a subclass of schedulers in timed systems., Presburger liveness verification of discrete timed automata., Eliminating the storage tape in reachability constructions., Decidability and complexity of action-based temporal planning over dense time, Probabilistic state estimation for labeled continuous time Markov models with applications to attack detection, Concurrency in timed automata, Bisimulation for Feller-Dynkin processes, Updatable timed automata, An automated system repair framework with signal temporal logic, Temporal reasoning through automatic translation of tock-CSP into timed automata, Minimization of the number of clocks for timed scenarios, Waiting nets, Untangling the graphs of timed automata to decrease the number of clocks, Flexible nets: a modeling formalism for dynamic systems with uncertain parameters, Time-optimal control of large-scale systems of systems using compositional optimization, Twenty years of rewriting logic, Exploiting timed automata based fuzzy controllers for designing adaptive intrusion detection systems, A study on shuffle, stopwatches and independently evolving clocks, Composition methods for constructing characteristic formulas for dense-time models, Reo + \(\mathrm{mCRL2}\): a framework for model-checking dataflow in service compositions, Checking noninterference in timed CSP, Model-checking timed automata with deadlines with Uppaal, PuRSUE -- from specification of robotic environments to synthesis of controllers, Superposition as a decision procedure for timed automata, Modal event-clock specifications for timed component-based design, Computing branching distances with quantitative games, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Discrete-time control for rectangular hybrid automata, Operator precedence temporal logic and model checking, Model-checking precision agriculture logistics: the case of the differential harvest, Reachability relations of timed pushdown automata, Multi-scale verification of distributed synchronisation, Learning Mealy machines with one timer, A design of GPU-based quantitative model checking, On the initialization of clocks in timed formalisms, Parameterized model checking of networks of timed automata with Boolean guards, Timeline-based planning over dense temporal domains, Intention as commitment toward time, Probabilistic timed graph transformation systems, On the semantics of polychronous polytimed specifications, Backward symbolic optimal reachability in weighted timed automata, Certifying emptiness of timed Büchi automata, Learning specifications for labelled patterns, On subgame perfect equilibria in turn-based reachability timed games, Computing maximally-permissive strategies in acyclic timed automata, Active learning of timed automata with unobservable resets, Optimal and robust controller synthesis using energy timed automata with uncertainty, Semantics of temporal constrained objects, Synthesis of distinguishing test cases for timed finite state machines, Quantitative evaluation of time-dependent Petri nets and applications to biochemical networks, Dense-choice counter machines revisited, Abstract state machines: a unifying view of models of computation and of system design frameworks, A game approach to determinize timed automata, The compound interest in relaxing punctuality, Optimal and robust controller synthesis. Using energy timed automata with uncertainty, Timed vacuity, Process algebra for hybrid systems, A process calculus BigrTiMo of mobile systems and its formal semantics, Weighted register automata and weighted logic on data words, An abstract model for proving safety of autonomous urban traffic, Toward an algebraic theory of systems, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, A hierarchical consistency framework for real-time supervisory control, Formal verification of timed synchronous dataflow graphs using lustre, Timed automata relaxation for reachability, Iterative bounded synthesis for efficient cycle detection in parametric timed automata, The containment problem for unambiguous register automata and unambiguous timed automata, Logical time control of concurrent DES, Revisiting reachability in polynomial interrupt timed automata, Action transducers and timed automata, Optimal work-conserving scheduler synthesis for real-time sporadic tasks using supervisory control of timed discrete-event systems, Behaviour equivalent max-plus automata for timed Petri nets under open-loop race-policy semantics, Dynamics of reputation in mobile agents systems and weighted timed automata, Costs and rewards in priced timed automata, Complexity issues for timeline-based planning over dense time under future and minimal semantics, Detectability of labeled weighted automata over monoids, Product interval automata, Dynamic data structures for timed automata acceptance, On the determinization of event-clock input-driven pushdown automata, Counter machines and verification problems., On probabilistic timed automata., Decidable integration graphs., A graph based semantics for logical functional diagrams in power plant controllers, Is your model checker on time? On the complexity of model checking for timed modal logics, Positive loop-closed automata: A decidable class of hybrid systems, Linear parametric model checking of timed automata, An efficient subsumption test pipeline for BS(LRA) clauses, \textsc{LTL} falsification in infinite-state systems, Decisiveness of stochastic systems and its application to hybrid models, Zone-based verification of timed automata: extrapolations, simulations and what next?, Monitoring timed properties (revisited), Bounded delay timed channel coding, Timed games with bounded window parity objectives, Efficient convex zone merging in parametric timed automata, Timed network games, Context-free timed formalisms: robust automata and linear temporal logics, Moded and continuous abstract state machines, Timed Petri nets with reset for pipelined synchronous circuit design, Interval probabilistic timed graph transformation systems, Timed-pNets: a communication behavioural semantic model for distributed systems, Semantic domains of timed event structures, Conformance testing for real-time systems, Discrete semantics for hybrid automata. Avoiding misleading assumptions in systems biology, Supervisory control of \((\max,+)\) automata: a behavioral approach, Improved undecidability results on weighted timed automata, Formal verification of real-time systems with preemptive scheduling, Folk theorems on the determinization and minimization of timed automata, Robust parametric reachability for timed automata, State explosion in almost-sure probabilistic reachability, Modular design of real-time systems using hierarchical communicating real-time state machines, Verifying distributed real-time properties of embedded systems via graph transformations and model checking, Performance analysis of probabilistic timed automata using digital clocks, When are stochastic transition systems tameable?, On clock-aware LTL parameter synthesis of timed automata, How to stop time stopping, Analysis of a biphase mark protocol with Uppaal and PVS, Workload correlations in multi-processor hard real-time systems, Time-abstracted bisimulation: Implicit specifications and decidability, Event algebra for transition systems composition application to timed automata, Passive testing with asynchronous communications and timestamps, Reachability analysis of dynamical systems having piecewise-constant derivatives, On the freeze quantifier in Constraint LTL: Decidability and complexity, Axiomatisation and decidability of multi-dimensional Duration Calculus, Hybridization methods for the analysis of nonlinear systems, Symbolic models for control systems, An automata-theoretic approach to constraint LTL, Wireless protocol validation under uncertainty, Parametric probabilistic transition systems for system design and analysis, Semantics and pragmatics of real-time maude, Timed automata and recognizability, On the rational behaviors of concurrent timers, \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics, Probabilistic timed automata with clock-dependent probabilities, Finite automata on timed \(\omega\)-trees, An algebraic approach to data languages and timed languages, Approximating labelled Markov processes, Automata over continuous time, The power of reachability testing for timed automata, Parameterized verification of time-sensitive models of ad hoc network protocols, An SMT-based approach to satisfiability checking of MITL, Verification in loosely synchronous queue-connected discrete timed automata., Generalized discrete timed automata: Decidable approximations for safety verification., Pushdown timed automata: A binary reachability characterization and safety verification., Controller synthesis for dynamic hierarchical real-time plants using timed automata, Execution information rate for some classes of automata, Accelerating worst case execution time analysis of timed automata models with cyclic behaviour, Synthesizing bounded-time 2-phase fault recovery, Bounded determinization of timed automata with silent transitions, Timed-automata abstraction of switched dynamical systems using control invariants, Verification and control of partially observable probabilistic systems, Generalizing input-driven languages: theoretical and practical benefits, System theory for system identification., On the timed temporal logic planning of coupled multi-agent systems, Past pushdown timed automata and safety verification., Scheduling hard sporadic tasks with regular languages and generating functions., Hybrid I/O automata., Checking temporal duration properties of timed automata., Timed discrete event control of parallel production lines with continuous outputs, Model checking duration calculus: a practical approach, Codiagnosability of discrete event systems revisited: a new necessary and sufficient condition and its applications, Refinement to imperative HOL, When are timed automata weakly timed bisimilar to time Petri nets?, Automatic generation of path conditions for concurrent timed systems, Models and formal verification of multiprocessor system-on-chips, The language preservation problem is undecidable for parametric event-recording automata, Verification of qualitative \(\mathbb Z\) constraints, Unifying behavioral equivalences of timed transition systems, A process algebraic framework for specification and validation of real-time systems, Detecting synchronisation of biological oscillators by model checking, Hybrid automata, reachability, and systems biology, Model checking memoryful linear-time logics over one-counter automata, Model checking mobile stochastic logic, Inclusion dynamics hybrid automata, An algebra of hybrid systems, Approximately bisimilar symbolic models for nonlinear control systems, Towards a real-time distributed computing model, M-nets: a survey, Network invariants for real-time systems, On minimal elements of upward-closed sets, What's decidable about hybrid automata?, Event-clock automata: a determinizable class of timed automata, Straightening out rectangular differential inclusions, Post and pre-initialized stopwatch Petri nets: formal semantics and state space computation, Robust safety of timed automata, Timed verification of the generic architecture of a memory circuit using parametric timed automata, \(\varepsilon\)-transitions in concurrent timed automata, A Kleene theorem for splitable signals, On the complexities of selected satisfiability and equivalence queries over Boolean formulas and inclusion queries over hulls, Decision problems for lower/upper bound parametric timed automata, A quadratic-time DBM-based successor algorithm for checking timed automata, Timed automata and additive clock constraints, Refinement of time, Deductive verification of real-time systems using STeP, PLC-automata: A new class of implementable real-time automata, Automatic verification of real-time systems with discrete probability distributions., Bisimulation indexes and their applications, Decidable verification for reducible timed automata specified in a first order logic with time, Efficiency of asynchronous systems, read arcs, and the MUTEX-problem, Specification of real-time and hybrid systems in rewriting logic, Deterministic delay analysis of AVB switched Ethernet networks using an extended trajectory approach, The Newton and Coulomb laws as information transfer by virtual particles, Continuity controlled hybrid automata, Periodicity based decidable classes in a first order timed logic, Counterexample-guided predicate abstraction of hybrid systems, Scheduling with timed automata, Schedulability analysis of fixed-priority systems using timed automata, Efficient timed model checking for discrete-time systems, A survey of temporal data mining, Unnamed Item, Algorithmic analysis of polygonal hybrid systems. I: Reachability, Symbolic model checking for probabilistic timed automata, Synthesising succinct strategies in safety games with an application to real-time scheduling, Parameter synthesis for probabilistic timed automata using stochastic game abstractions, Towards a formal semantics for UML/MARTE state machines based on hierarchical timed automata, Shrinking timed automata, Timed substitutions for regular signal-event languages, On the optimal reachability problem of weighted timed automata, On the expressiveness and decidability of o-minimal hybrid systems, Predictable real-time software synthesis, Predicate diagrams for the verification of real-time systems, Task automata: Schedulability, decidability and undecidability, Switched discrete-time systems with time-varying delays: A generalized \(\mathcal H_2\)-approach, A Petri net approach for the design and analysis of web services choreographies, POETS: process-oriented event-driven transaction systems, Schedulability of asynchronous real-time concurrent objects, Modelling and analysis of normative documents, Predictive runtime enforcement, Polynomial interrupt timed automata: verification and expressiveness, Information rate of some classes of non-regular languages: an automata-theoretic approach, Computational techniques for reachability analysis of Max-Plus-Linear systems, Understand volatility of algorithmic stablecoin: modeling, verification and empirical analysis, Dealing with practical limitations of distributed timed model checking for timed automata, Zeno hybrid systems, TCTL-preserving translations from timed-arc Petri nets to networks of timed automata, Efficient modeling of MIMO systems through timed automata based neuro-fuzzy inference engine, Cost enforcement in the real-time specification for Java, Characteristic Formulae for Timed Automata, Taylor approximation for hybrid systems, On a decision procedure for quantified linear programs, WCET free time analysis of hard real-time systems on multiprocessors: A regular language-based model, Towards general axiomatizations for bisimilarity and trace semantics, A zero-space algorithm for negative cost cycle detection in networks, Algorithmic analysis of polygonal hybrid systems. II: Phase portrait and tools, An extension of the inverse method to probabilistic timed automata, Event clock message passing automata: a logical characterization and an emptiness checking algorithm, Time-triggered runtime verification, Model checking for probabilistic timed automata, A compositional modelling and analysis framework for stochastic hybrid systems, On-the-fly verification and optimization of DTA-properties for large Markov chains, Modelling temporal behaviour in complex systems with Timebands, Formal verification of multitasking applications based on timed automata model, Optimal infinite scheduling for multi-priced timed automata, Timed Petri nets and timed automata: On the discriminating power of Zeno sequences, Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\), Analysis of dynamic policies, A decidable class of planar linear hybrid systems, Monotonic hybrid systems, A control synthesis approach for time discrete event systems, Grid automata and supervisory control of dense real-time discrete event systems, Refinement of actions for real-time concurrent systems with causal ambiguity, On model-checking timed automata with stopwatch observers, On the expressiveness of TPTL and MTL, Optimal control of discrete-time hybrid automata under safety and liveness constraints, Model checking restricted sets of timed paths, LTL over integer periodicity constraints, State estimation of max-plus automata with unobservable events, Bisimulation for labelled Markov processes, Remove irrelevant atomic formulas for timed automaton model checking, Statistical probabilistic model checking with a focus on time-bounded properties, Verifying untimed and timed aspects of the experimental batch plant, Computing efficient operation schemes for chemical plants in multi-batch mode, Categories of Timed Stochastic Relations, Combining free choice and time in Petri nets, Consistency in parametric interval probabilistic timed automata, Generalized rewrite theories, coherence completion, and symbolic methods, Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata, A Perfect Class of Context-Sensitive Timed Languages, Complexity Hierarchies beyond Elementary, Formalized Timed Automata, Timed $$\pi $$-Calculus, On composition and lookahead delegation of \(e\)-services modeled by automata, Input urgent semantics for asynchronous timed session types, A symbolic decision procedure for cryptographic protocols with time stamps, Conditional simple temporal networks with uncertainty and decisions, Effective definability of the reachability relation in timed automata, A partial order semantics approach to the clock explosion problem of timed automata, A theory of stochastic systems. I: Stochastic automata, A theory of stochastic systems. II: Process algebra, Safe diagnosability for fault-tolerant supervision of discrete-event systems, Sampling automata and programs, Entropy of regular timed languages, Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques, Expand, enlarge and check: new algorithms for the coverability problem of WSTS, Reachability in two-clock timed automata is PSPACE-complete, A maximal entropy stochastic process for a timed automaton, Unwinding biological systems, On the expressivity of time-varying graphs, Abstraction and approximation in fuzzy temporal logics and models, Checking conformance for time-constrained scenario-based specifications, Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions, Transformations for Compositional Verification of Assumption-Commitment Properties, Language Emptiness of Continuous-Time Parametric Timed Automata, Safe and Optimal Adaptive Cruise Control, A Logical Encoding of Timed $$\pi $$-Calculus, Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions, Solving the time varying postman problems with timed automata, Checking Integral Real-Time Automata for Extended Linear Duration Invariants, From Safety Critical Java Programs to Timed Process Models, Automated Reasoning for Hybrid Systems — Two Case Studies —, Equivalence checking and intersection of deterministic timed finite state machines, Automated repair for timed systems, Distributed parametric model checking timed automata under non-zenoness assumption, Human-cyber-physical automata and their synthesis, Diagnosis of timed patterns for discrete event systems by means of state isolation, An efficient customized clock allocation algorithm for a class of timed automata, On specifications and proofs of timed circuits, Asynchronous correspondences between hybrid trajectory semantics, Simulation relations and applications in formal methods, Approximating Continuous Systems by Timed Automata, Linear Time Monitoring for One Variable TPTL, Temporal Robustness of Stochastic Signals, ETCetera: beyond Event-Triggered Control, Updatable Timed Automata with Additive and Diagonal Constraints, Optimal controller synthesis for timed systems, Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets, Parametric updates in parametric timed automata, Spiking neural networks modelled as timed automata: with parameter learning, revTPL: The Reversible Temporal Process Language, Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic, Timed Control with Observation Based and Stuttering Invariant Strategies, Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems, Learning deterministic one-clock timed automata via mutation testing, Active learning of one-clock timed automata using constraint solving, Repairing real-time requirements, A space-efficient on-the-fly algorithm for real-time model checking, State equivalences for rectangular hybrid automata, Verifying abstractions of timed systems, Equivalence checking 40 years after: a review of bisimulation tools, Spatial and timing properties in highway traffic, History-deterministic timed automata are not determinizable, Probabilistic verification of diagnosability for a certain class of timed stochastic systems, Energy Büchi problems, Abstract Interpretation with Applications to Timing Validation, Waiting Nets: State Classes and Taxonomy, Diagnosability of fault patterns with labeled stochastic Petri nets, Pattern Matching and Parameter Identification for Parametric Timed Regular Expressions, Dynamic controllability of temporal networks with instantaneous reaction, STORMED Hybrid Systems, Placement Inference for a Client-Server Calculus, Learning Meets Verification, ON COUNTER MACHINES, REACHABILITY PROBLEMS, AND DIOPHANTINE EQUATIONS, When Is Reachability Intrinsically Decidable?, Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions, Distributed Timed Automata with Independently Evolving Clocks, Some Recent Results in Metric Temporal Logic, Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets, Concavely-Priced Timed Automata, Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets, Timed Automata with Integer Resets: Language Inclusion and Expressiveness, On Scheduling Policies for Streams of Structured Jobs, Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains, On Conformance Testing for Timed Systems, A new method for centralised and modular supervisory control of real-time discrete event systems, CONTINUOUS PETRI NETS: EXPRESSIVE POWER AND DECIDABILITY ISSUES, Event-Clock Visibly Pushdown Automata, Learning Mealy machines with one timer, Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format, Branching Time Semantics for UML 2.0 Sequence Diagrams, Extending EFSMs to Specify and Test Timed Systems with Action Durations and Timeouts, Scenario-Based Timing Consistency Checking for Time Petri Nets, Specification of Timed EFSM Fault Models in SDL, Improvements for the Symbolic Verification of Timed Automata, Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata, Survey on Directed Model Checking, Analysis of Linear Hybrid Systems in CLP, Interrupt Timed Automata, Minimal Cost Reachability/Coverability in Priced Timed Petri Nets, Refinement and Consistency of Timed Modal Specifications, Determinization and Expressiveness of Integer Reset Timed Automata with Silent Transitions, One-Clock Deterministic Timed Automata Are Efficiently Identifiable in the Limit, Design and Verification of Fault-Tolerant Components, Highly Undecidable Problems For Infinite Computations, Weighted versus Probabilistic Logics, Property Driven Three-Valued Model Checking on Hybrid Automata, AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA, Linear-time temporal logics with Presburger constraints: an overview ★, Volume and Entropy of Regular Timed Languages: Analytic Approach, Synthesis of Non-Interferent Timed Systems, Speeding Up Model Checking of Timed-Models by Combining Scenario Specialization and Live Component Analysis, Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation, Model Checking Logic WCTL with Multi Constrained Modalities on One Clock Priced Timed Automata, Removing All Silent Transitions from Timed Automata, Realizability of Real-Time Logics, Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata, A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata, Checking Timed Büchi Automata Emptiness Using LU-Abstractions, Modelling and hierarchical diagnosis of timed discrete-event systems, Conformance Testing Relations for Timed Systems, Formal design and analysis of a hybrid supervisory control structure for Virtual Production Systems, Refinement of Timing Constraints for Concurrent Tasks with Scheduling, Control Strategies for Off-Line Testing of Timed Systems, Lazy Reachability Checking for Timed Automata with Discrete Variables, Quantitative Model Checking for a Controller Design, A case study on parametric verification of failure detectors, Modularity for timed and hybrid systems, Reachability analysis of pushdown automata: Application to model-checking, Reconfigurable timed graphs for the design of optimal scheduling in uncertain environments based on transition-timed Petri net, The tail-recursive fragment of timed recursive CTL, Modeling and analysis of switching max-plus linear systems with discrete-event feedback, Testing membership for timed automata, Cross-chain payment protocols with success guarantees, Control strategies for off-line testing of timed systems, Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties, Bridging the gap between single- and multi-model predictive runtime verification, Unnamed Item, Unnamed Item, Timed Basic Parallel Processes, Testing timed automata, Fast asynchronous systems in dense time, Metric semantics for true concurrent real time, Locally finite languages, Well-structured transition systems everywhere!, Symbolic reachability computation for families of linear vector fields, A first order logic for specification of timed algorithms: Basic properties and a decidable class, A polynomial-time algorithm for checking equivalence under certain semiring congruences motivated by the state-space isomorphism problem for hybrid systems, Process algebra for performance evaluation, Model checking for a class of weighted automata, The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism, Optimal run problem for weighted register automata, Abstraction refinement and antichains for trace inclusion of infinite state systems, Weak Cost Register Automata are Still Powerful, Timed Bounded Verification of Inclusion Based on Timed Bounded Discretized Language, Abstraction in Fixpoint Logic, Safe Decomposition of Startup Requirements: Verification and Synthesis, Verified Certification of Reachability Checking for Timed Automata, Learning One-Clock Timed Automata, Skill-Based Verification of Cyber-Physical Systems, Lossiness of communication channels modeled by transducers1, Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities, The p-adic Theory of Automata Functions, Efficient scaling-invariant checking of timed bisimulation, Removing ε-transitions in timed automata, Model-checking for real-time systems, From finite automata toward hybrid systems (Extended abstract), On the Modeling of Sequential Reactive Systems by Means of Real Time Automata, Unnamed Item, Bisimulation on speed: Lower time bounds, LTL Parameter Synthesis of Parametric Timed Automata, A decidable timeout-based extension of linear temporal logic, Symbolic timing devices, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Abstractions Refinement for Hybrid Systems Diagnosability Analysis, Unnamed Item, Unnamed Item, Timed P Automata, Unnamed Item, A Logical Characterisation of Event Clock Automata, Unnamed Item, Progress-preserving Refinements of CTA, Universal safety for timed Petri nets is PSPACE-complete, MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS, Model Checking Biological Oscillators, Hybrid Automata in Systems Biology: How Far Can We Go?, Hybrid automata with finite bisimulations, The expressive power of clocks, Automatic synthesis of real time systems, ADVANCED SYNCHRONIZATION OF AUDIO OR SYMBOLIC MUSICAL PATTERNS: AN ALGEBRAIC APPROACH, Model Checking Quantitative Linear Time Logic, The Unmet Challenge of Timed Systems, Decomposition of timed automata for solving scheduling problems, THREE APPLICATIONS TO RATIONAL RELATIONS OF THE HIGH UNDECIDABILITY OF THE INFINITE POST CORRESPONDENCE PROBLEM IN A REGULAR ω-LANGUAGE, Compositional Design of Stochastic Timed Automata, A menagerie of timed automata, Approximate Verification of the Symbolic Dynamics of Markov Chains, Reachability in Timed Counter Systems, An Automata-based Approach for CTL⋆ With Constraints, On Resource-Sensitive Timed Component Connectors, Unnamed Item, Formal language properties of hybrid systems with strong resets, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Handling contingency in temporal constraint networks: from consistency to controllabilities, Unnamed Item, Unnamed Item, What’s Decidable About Parametric Timed Automata?, On Reachability Games of Ordinal Length, Distributed Event Clock Automata, Unnamed Item, Unnamed Item, Checking Temporal Properties of Discrete, Timed and Continuous Behaviors, Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking, A Kleene-Schützenberger Theorem for Weighted Timed Automata, Robust Analysis of Timed Automata Via Channel Machines, Probabilistic and Topological Semantics for Timed Automata, Automata and Logics for Timed Message Sequence Charts, Unnamed Item, Unnamed Item, Unnamed Item, An Introduction to Timed Automata, Supervisory target control for hybrid systems, Symbolic Approximation of Weighted Timed Games, Wireless ventilation control for large‐scale systems: The mining industrial case, An Inverse Method for Parametric Timed Automata, Approximated Reachability on Hybrid Automata: Falsification meets Certification, Model-checking Timed Temporal Logics, A game approach to the parametric control of real-time systems, SAT-BASED MODEL CHECKING FOR REGION AUTOMATA, On the Supports of Recognizable Timed Series, Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*, Discrete-Event Systems Fault Diagnosis, Towards an Efficient Tree Automata based technique for Timed Systems, Hierarchical hybrid modelling and control of an unmanned helicopter, ON REACHABILITY AND SAFETY IN INFINITE-STATE SYSTEMS, Verification of Linear Duration Invariants by Model Checking CTL Properties, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Discrete-time control for rectangular hybrid automata, Simulation Relations and Controllability Properties of Linear and Nonlinear Control Systems, Formal Analysis of Leader Election in MANETs Using Real-Time Maude, Unnamed Item, Control and synthesis of non-interferent timed systems, State feedback control of real-time discrete event systems with infinite states, Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets, A Survey on Analog Models of Computation, Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints*, Parametric Analyses of Attack-fault Trees*, Cost Problems for Parametric Time Petri Nets*, Formal analysis and control of timed automata with guards using (max, +) and (min, +) algebras

Cites Work

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:1322162&oldid=13447801"