Search

Copyright of Control Theory & Applications / Kongzhi Lilun Yu Yinyong is the property of Editorial Department of Control Theory & Applications and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

Deadlocks are of paramount importance in resource allocation systems, which are usually treated from the perspective of discrete event systems. This paper develops a deadlock prevention strategy for a system modeled with Petri nets, by endowing appropriate time constraints with certain transitions to schedule the firing priority of enabled transitions in a Petri net such that transition sequences leading to deadlocks are prohibited, i.e., expanding an untimed Petri net model into a time Petri net to prevent deadlocks. To increase the system permissiveness of a time Petri net with time constraints endowed, a control place is designed, which does not expand the reachable space of the original Petri net. The predominant role of the control place is to convert continuously enabled transitions at certain markings into newly enabled transitions, which can prolong the firing time of transitions. Furthermore, we propose a method that merely enumerates deadlock prevention condition inequalities to derive a series of time constraints by probing the connection between deadlock prevention conditions and transitions. The developed method only needs to designate time constraints for partial transitions. Examples are provided to demonstrate the effectiveness of the presented methodology.

This paper presents an approach to solve the least-cost transition sequences estimation problem in labelled time Petri net (LTPN) systems with unobservable transitions. Particularly, the considered LTPN system is bounded, in which each transition has a nonnegative cost and is labelled as either observable or unobservable. We first introduce a graph, called a segmented modified state class graph (SMSCG), that is a compact representation of the partial state space of an LTPN system. Based on the SMSCG and an observed time-label sequence, a method to estimate logic consistent transition sequences is proposed. By exploiting the transitions-related timing constraints in SMSCGs, a procedure for determining which logic consistent transition sequences are timing consistent with the observed time-label sequence and a given time is reported. Finally, we develop an algorithm to perform the estimation of least-cost transition sequences. [ABSTRACT FROM AUTHOR]

In order to adapt to the development trend of the communication based train control (CBTC) system from train-ground communication mode to train-to-train communication mode, a verification approach for time constraints of multi-period applications concurrence on-board safety computer based on time Petri net was proposed. By taking the double 2 out of 2 on-board safety computer as an example, the multi-period applications concurrence nature of the safety computer was analyzed. Time Petri net (TPN) was utilized to calculate the time schedulable interval. Then several cases were analyzed based on the inference of this approach. The analysis and verification results indicate that onboard safety computer can meet the time constraints of more than three periodic safety-critical applications under the condition of single-core with main frequency of 1GHz, which demonstrates the effectiveness of verifying and evaluating the time constraints of safety computer periodic applications using TPN.

This paper is about control sequences design for Discrete Event Systems (DES) modeled with Time Petri nets (TPN) including a set of temporal specifications. Petri nets are known as efficient mathematical and graphical models that are widely used to describe distributed DES including choices, synchronizations and parallelisms. The domains of application include but are not restricted to manufacturing systems, computer science and transportation networks. Incorporating the time in the model is important to consider many control problems such as scheduling and planning. This paper solves some control issues in timed context and uncertain environments that include unexpected events modeled with uncontrollable transitions. To deal with such uncertainties, we propose first to build an Approximated Timed Reachability Graph that includes the time specifications and model all feasible timed trajectories at a given accuracy under earliest firing policy. Then, this graph is used to search optimal paths by using an approach based on Markov Decision Processes that encode the environment uncertainties. Such optimal paths lead to near-optimal solutions for the TPN. Several simulations illustrate the benefit of the proposed method from the performance and computational points of view. [ABSTRACT FROM AUTHOR]

Copyright of China Mechanical Engineering is the property of Editorial Board of China Mechanical Engineering and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

Copyright of Journal on Communication / Tongxin Xuebao is the property of Journal on Communications Editorial Office and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

Level crossing (LC) safety is a crucial issue for railway operators and infrastructure managers. Accidents at LCs give rise to serious material and human damage, while seriously impacting the reputation of railway safety. In particular, some typical scenarios are behind the main part of train-car collisions, which occur at LCs. On the other hand, European Rail Traffic Management System (ERTMS) is the standard railway control-command and signaling system that is currently being implemented throughout Europe and elsewhere. The aim is to ensure railway interoperability while enhancing safety and competitiveness of the railway transportation. ERTMS specifications only provide a rough description when dealing with LC control. This paper elaborates on a functional control architecture for automatic LCs in the context of ERTMS operation Levels 2 and 3. Indeed, these operation levels ensure a continuous knowledge of train location thanks to the Global System for Mobile Communications—Railways link between the trains and the Radio Block Center. Hence, the established LC control scheme aims to ensure an optimal LC command based on the information regarding the train location and, thereby, prevent some potential risky scenarios and improve the global safety at LCs. To achieve this, a generic methodology is employed. First, a formal behavioral model is developed using the time Petri net (TPN) notation. Then, the problem is formalized on the basis of the established TPN, in such a way as to carry out a sound and trustworthy analysis. The various steps of the developed approach are detailed and illustrated in the course of this paper. To the best of our knowledge, this is the first work that seeks to elaborate a control strategy of automatic LC in the ERTMS operation context. [ABSTRACT FROM PUBLISHER]

Mission assurance policy and risk management are essential in enabling decision makers to ensure successful completion of missions by addressing the security status of cyber assets. This paper presents a novel mission assurance policy that adapts to the dynamic security status of all mission assets to quickly and automatically determine mission assurance level and to decide what changes are needed accordingly. The novelty of this mission assurance policy stems from using a time Petri net model for determining the security status of cyber assets, and then employing binary or multi-valued logic decision diagrams to assess the mission assurance level. The ability of a mission assurance policy to successfully complete its objectives depends mainly on whether a risk management scheme is provided to reduce risk to an acceptable level. To that end, this paper also describes a risk management scheme to systematically deal with the main factors of risk management such as the temporal interdependencies of cyber assets, impact of attacks, and risk mitigation. Given that the status of cyber assets changes due to the dynamic cybersecurity environment of asset vulnerabilities, threats, and recovery, the proposed mission assurance policy and risk management scheme enable decision makers to cope with the real-time assessment of mission assurance level. [ABSTRACT FROM AUTHOR]

Computer system reliability is conventionally modeled and analyzed using techniques such as fault tree analysis and reliability block diagrams (RBDs), which provide static representations of system reliability properties. A recent extension to RBDs, called dynamic RBDs (DRBD), defines a framework for modeling the dynamic reliability behavior of computer-based systems. However, analyzing a DRBD model in order to locate and identify design errors, such as a deadlock error or faulty state, is not trivial when done manually. A feasible approach to verifying it is to develop its formal model and then analyze it using programmatic methods. In this paper, we first define a reliability markup language that can be used to formally describe DRBD models. Then, we present an algorithm that automatically converts a DRBD model into a colored Petri net. We use a case study to illustrate the effectiveness of our approach and demonstrate how system properties of a DRBD model can be verified using an existing Petri net tool. Our formal modeling approach is compositional; thus, it provides a potential solution to automated verification of DRBD models. [ABSTRACT FROM AUTHOR]

We consider Time Petri Nets (TPN) for which a firing time interval is associated with each transition. State space abstractions for TPN preserving various classes of properties (LTL, CTL and CTL∗) can be computed, in terms of so called state classes. Some methods were proposed to check quantitative timed properties but are not suitable for effective verification of properties of real-life systems. In this article, we consider subscript TCTL for TPN (TPN-TCTL) for which temporal operators are extended with a time interval, specifying a time constraint on the firing sequences. We prove the decidability of TPN-TCTL on bounded TPN and give its theoretical complexity. We propose a zone-based state space abstraction that preserves marking reachability and traces of the TPN. As for Timed Automata (TA), the abstraction may use an over-approximation operator on zones to enforce the termination. A coarser (and efficient) abstraction is then provided and proved exact w.r.t. marking reachability and traces (LTL properties). Finally, we consider a subset of TPN-TCTL properties (TPN-TCTLS) for which it is possible to propose efficient on-the-fly model-checking algorithms. Our approach consists in computing and exploring the zone-based state space abstraction. On a practical point of view, the method is integrated in Romeo [Gardey et al. (2005, Proceedings of 17th International Conference on CAV’05, Vol. 3576 of Lecture Notes in Computer Science, 418–423)], a tool for TPN edition and analysis. In addition to the old features it is now possible to effectively verify a subset of TCTL directly on TPN. [ABSTRACT FROM PUBLISHER]

This paper investigates the deadlock prevention problem for Petri nets (PN), in which the control is performed by appropriately setting time constraints on transitions, in terms of firing intervals. We show that this time based deadlock prevention (TBDP) problem is decidable for bounded PN and can be formalised as a parametric model checking problem. However, in this context, the parametric model checking faces a severe state explosion problem. To deal with this limitation, we propose a symbolic approach that abstracts firing order constraints and bypasses the use of parameter domains with their associated very costly operations. Both approaches can handle, as an input model, a (time) PN with controllable/uncontrollable transitions. In such a case, they expose whether or not the firing intervals of the controllable transitions of the input model can be restricted so as to force the deadlock freeness (i.e., there is no marking with no enabled transitions). [ABSTRACT FROM AUTHOR]

In this paper, we propose an enumerative approach to build the state class graph of the TSPN (Time Stream Petri Net) model. A TSPN model is a Petri net augmented with intervals on arcs and synchronization rules on transitions. It can be used to model complex systems, and it is proved to be more expressive than TPN (Time Petri Nets). In contrast with TPN where each class accessible in the graph is given as a pair (M,D) where M is a marking and D is a system of DBM inequalities, a TSPN class in this form is much complex to compute. To tackle this issue, we introduce a new formalism called the time distance function to define a TSPN class. This function makes it possible to determine an efficient algorithm to compute each class of the graph in a square complexity time. Finally, we show how to exploit the TSPN state class graph (when finite), to check over either linear properties of the model, or to compute minimal and maximal time distances of any firing sequence. [ABSTRACT FROM AUTHOR]

In this paper we propose an approach of multimedia scenarios management in an object-relational database system that considers three main aspects: an object-oriented method for multimedia scenarios modeling, time-interval and causal relations models for the specification of multimedia objects with fixed or unknown playout durations, and interactive and dependency temporal relations. Based on the user's temporal specification, a time Petri net (PN) is automatically generated and translated to the formalism of the verification tool Tina, which allows analyzing multimedia scenarios specification. Finally, we evaluate our approach with an experimental system prototype. The originality of the approach proposed is to consider: a temporal specification that combines interval-based model and temporal dependency (causality) between intervals; temporal specification based on PN, that extracts errors that are too difficult to extract manually; and finally temporal intervals with known or unknown time. [ABSTRACT FROM AUTHOR]

In this paper, we define a model dedicated to the specification of multimedia applications called Preemptive Time Petri Nets with synchronizing transitions (STPTPN) as an extension of T-time Petri nets where time is associated with transitions. The model is proposed in the general purpose to model a large scale of multimedia requirements. Thus, resource requirement issues are discussed in this paper, and addressed in the model. To deal with, resources are modelled as special places using a new mechanism called preemptor hyperarc which lets a transition be resource strongly -- enabled, resource -- violated or resource -- violating. Moreover, two additional mechanisms are considered: A time suspension mechanism that uses inhibitor arcs associated with stopwatches and synchronization mechanisms that allow the simultaneous firing of a set of transitions (called Rendezvous), according to different schemes. Compared to other existing models, our model is provided with an adapted semantics, designed to represent clearly and accurately time requirements, as well as the complex resource-preempting mechanisms that are observed in multimedia systems. [ABSTRACT FROM AUTHOR]

The paper proposes an approach to solving some verification problems of time Petri nets using linear programming. The approach is based on the observation that for loop-closed time Petri nets, it is only necessary to investigate a finite prefix of an untimed run of the underlying Petri net. Using the technique the paper gives solutions to reachability and bounded delay timing analysis problems. For both problems algorithms are given, that are decision procedures for loop-closed time Petri nets, and semi-decision procedures for general time Petri nets. [ABSTRACT FROM AUTHOR]

In this paper, a parametric description of a transition sequence in a Time Petri net is introduced. The minimal and maximal time duration of a transition sequence are shown to be integers and furthermore the min/max path passes only integer-states. A necessary condition for the reachability of an arbitrary state is given. [ABSTRACT FROM AUTHOR]

Standard Petri nets are an untimed logical model. But timing information is important for real-time control of discrete event systems. This paper studies stale feeds beck control of concurrent discrete event systems modeled by controlled time Petri nets. It is assumed that a control specification is given in terms of markings. A maximal element of the set of controllers achieving a control specification is called a maximally permissive controller (MPC). In general, the MPC is not necessarily unique in controlled time Petri nets. In this paper, we present a necessary as sufficient condition for the unique existence of the maximally permissive controller. Then we derive a closed form expression of the unique MPC if it exists. Moreover, we synthesize a unique MPC for a simple manufacturing system. [ABSTRACT FROM AUTHOR]

• Defines a new verification method supporting real-time property specification. • Focuses on the composability of expressiveness and the performance of verification. • Achieves several orders of magnitude improvement in the verification cost. We define a new verification method, called RT-MOBS, for checking real-time requirements based on Time Petri nets (TPN). Our approach supports requirements specified using a very expressive pattern language, the Property Specification Language (PSL) of Autili, Grusnke et al., and relies on marking observers' verification. RT-MOBS has many distinctive features, such as a focus on performances, a compositional method for deriving the observer and the target property directly from the structure of the specification pattern, and the ability to deal with the whole real-time fragment of PSL. We demonstrate the effectiveness of our approach from three industrial use cases: a mobile ad-hoc network system; the model of a flight management system, which is realistic with respect to the industry use during the architecture evaluation phase; and a model of an order to cash smart contract. Our experimental results show that we can achieve performances that are several orders of magnitude better than with methods based on an interpretation of patterns into Linear Temporal Logic (LTL) formulas. [ABSTRACT FROM AUTHOR]