The TLL XYZ/E is a formal language able to represent the dynamic semantics and the static semantics in a unified framework. It supports the whole process of program development, i.e. from the abstract specification to...The TLL XYZ/E is a formal language able to represent the dynamic semantics and the static semantics in a unified framework. It supports the whole process of program development, i.e. from the abstract specification to the efficiently executable program in a formal, precise and convenient way. The steam boiler control specification problem, a large case study in the fields of real time, hybrid and communication systems, is discussed with XYZ/E. The approach covers physical model construction, formal specification, stepwise refinement, verification, executable program and visual user interface programming.展开更多
This paper investigates control synthesis for motion planning under conditions of uncertainty,specifically in robot motion and environmental properties,which are modeled using a probabilistic labeled Markov decision p...This paper investigates control synthesis for motion planning under conditions of uncertainty,specifically in robot motion and environmental properties,which are modeled using a probabilistic labeled Markov decision process(PL-MDP).To address this,a model-free reinforcement learning(RL)approach is designed to produce a finite-memory control policy that meets complex tasks specified by linear temporal logic(LTL)formulas.Recognizing the presence of uncertainties and potentially conflicting objectives,this study centers on addressing infeasible LTL specifications.A relaxed LTL constraint enables the agent to adapt its motion plan,allowing for partial satisfaction by accounting for necessary task violations.Additionally,a new automaton structure is introduced to increase the density of accepting rewards,facilitating deterministic policy outcomes.The proposed RL framework is rigorously analyzed and prioritizes two key objectives:(1)satisfying the acceptance condition of the relaxed product MDP,and(2)minimizing long-term violation costs.Simulation and experimental results are presented to demonstrate the framework’s effectiveness and robustness.展开更多
In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge...In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system＇s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.展开更多
Model checking based on linear temporal logic reduces the false negative rate of misuse detection.However,linear temporal logic formulae cannot be used to describe concurrent attacks and piecewise attacks.So there is ...Model checking based on linear temporal logic reduces the false negative rate of misuse detection.However,linear temporal logic formulae cannot be used to describe concurrent attacks and piecewise attacks.So there is still a high rate of false negatives in detecting these complex attack patterns.To solve this problem,we use interval temporal logic formulae to describe concurrent attacks and piecewise attacks.On this basis,we formalize a novel algorithm for intrusion detection based on model checking interval temporal logic.Compared with the method based on model checking linear temporal logic,the new algorithm can find unknown succinct attacks.The simulation results show that the new method can effectively reduce the false negative rate of concurrent attacks and piecewise attacks.展开更多
In this paper,w e provide a novel scheme to solve the motion planning problem of multi-agent systems under high-level task specifications.First,linear temporal logic is applied to express the global task specification...In this paper,w e provide a novel scheme to solve the motion planning problem of multi-agent systems under high-level task specifications.First,linear temporal logic is applied to express the global task specification.Then an efficient and decentralized algorithm is proposed to decom pose it into local tasks.M oreover,w e use control barrier function to synthesize the local controller for each agent under the linear temporal logic motion plan with safety constraint.Finally,simulation results show the effectiveness and efficiency of our proposed scheme.展开更多
To combat the well-known state-space explosion problem in Prop ositional Linear T emp o- ral Logic （PLTL） model checking, a novel algo- rithm capable of translating PLTL formulas into Nondeterministic Automata （NA...To combat the well-known state-space explosion problem in Prop ositional Linear T emp o- ral Logic （PLTL） model checking, a novel algo- rithm capable of translating PLTL formulas into Nondeterministic Automata （NA） in an efficient way is proposed. The algorithm firstly transforms PLTL formulas into their non-free forms, then it further translates the non-free formulas into their Normal Forms （NFs）, next constructs Normal Form Graphs （NFGs） for NF formulas, and it fi- nally transforms NFGs into the NA which ac- cepts both finite words and int-mite words. The experimental data show that the new algorithm re- duces the average number of nodes of target NA for a benchmark formula set and selected formulas in the literature, respectively. These results indi- cate that the PLTL model checking technique em- ploying the new algorithm generates a smaller state space in verification of concurrent systems.展开更多
Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a...Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a fair timed automaton （TA） that recognizes its satisfying models with prototype verification system （PVS） in this paper. Both the tabular construction＇s principles and the PVS implementation details are given for the different type of MITL formula according to the corresponding semantics interpretations. After this transformation procedure, specifications expressed with MITL formula can be verified formally in the timed automata framework developed previously.展开更多
Linear temporal logic(LTL)is an intuitive and expressive language to specify complex control tasks,and how to design an efficient control strategy for LTL specification is still a challenge.In this paper,we implement ...Linear temporal logic(LTL)is an intuitive and expressive language to specify complex control tasks,and how to design an efficient control strategy for LTL specification is still a challenge.In this paper,we implement the dynamic quantization technique to propose a novel hierarchical control strategy for nonlinear control systems under LTL specifications.Based on the regions of interest involved in the LTL formula,an accepting path is derived first to provide a high-level solution for the controller synthesis problem.Second,we develop a dynamic quantization based approach to verify the realization of the accepting path.The realization verification results in the necessity of the controller design and a sequence of quantization regions for the controller design.Third,the techniques of dynamic quantization and abstraction-based control are combined together to establish the local-to-global control strategy.Both abstraction construction and controller design are local and dynamic,thereby resulting in the potential reduction of the computational complexity.Since each quantization region can be considered locally and individually,the proposed hierarchical mechanism is more efficient and can solve much larger problems than many existing methods.Finally,the proposed control strategy is illustrated via two examples from the path planning and tracking problems of mobile robots.展开更多
Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent syst...Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a guasi-classical temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. Our models are paraKripke structures (extended standard Kripke structures), in which both a formula and its negation are satisfied in a same state, and properties to be verified are expressed by QCTL with paraKripke structures semantics. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.展开更多
The paper proposed an approach to study the power system voltage coordinated control using Linear Temporal Logic (LTL). First, the hybrid Automata model for power system voltage control was given, and a hierarchical c...The paper proposed an approach to study the power system voltage coordinated control using Linear Temporal Logic (LTL). First, the hybrid Automata model for power system voltage control was given, and a hierarchical coordinated voltage control framework was described in detail. In the hierarchical control structure, the high layer is the coordinated layer for global voltage control, and the low layer is the power system controlled. Then, the paper introduced the LTL language, its specification formula and basic method for control. In the high layer, global voltage coordinated control specification was defined by LTL specification formula. In order to implement system voltage coordinated control, the LTL specification formula was transformed into hybrid Automata model by the proposed algorithms. The hybrid Automata in high layer could coordinate the different distributed voltage controller, and have constituted a closed loop global voltage control system satisfied the LTL specification formula. Finally, a simple example of power system voltage control include the OLTC controller, the switched capacitor controller and the under-voltage shedding load controller was given for simulating analysis and verification by the proposed approach for power system coordinated voltage control. The results of simulation showed that the proposed method in the paper is feasible.展开更多
Reachability-based analysis and temporal analysis are used to verify the properties of concurrent systems, and it is important to exploit fast and efficient methods. This paper gives semantics of temporal formulae wit...Reachability-based analysis and temporal analysis are used to verify the properties of concurrent systems, and it is important to exploit fast and efficient methods. This paper gives semantics of temporal formulae with edges of the transition system of Petri net, and then presents a fast temporal analyzing method, which takes advantage of both Petri net and temporal logic. The method only expands a path of equivalence trace while the path does not satisfy a property according to trace semantics of Petri net, and can validate directly the property on Petri net. Moreover, we exploit a minimal degree of in-out of a node as heuristics to select a path of an equivalence trace. Finally, we demonstrate the validity of the method that decreases state spaces and improves the verification system with the experimental results.展开更多
The traffic rules governing the passage of different types of vehicles at signal-free intersections are distinct,especially for the emergency vehicles.Although these traffic rules can be described through deliberate m...The traffic rules governing the passage of different types of vehicles at signal-free intersections are distinct,especially for the emergency vehicles.Although these traffic rules can be described through deliberate mathematical expressions,but showing limitations in terms of the userfriendliness of rule description.This paper proposes an improved STL-based trajectory planning method for CAVs at signal-free intersections,describing traffic rules with STL formulas,which bridges the gap between human-understandable and machine-understandable traffic rules.The MPC framework is utilised to guarantee real-time trajectory planning by reducing travel time of vehicles passing through the intersection.Simulation results show improved traffic efficiency compared with other methods while ensuring adherence to yielding rules for emergency CAVs.展开更多
This paper proposes a model predictive control(MPC)algorithm for a small satellite to accomplish on-orbit inspection missions.The relative dynamics of satellite is modelled first.Then,multiple constraints are taken in...This paper proposes a model predictive control(MPC)algorithm for a small satellite to accomplish on-orbit inspection missions.The relative dynamics of satellite is modelled first.Then,multiple constraints are taken into account for the on-orbit inspection missions,including input saturation,obstacle avoidance,velocity limit,and task specifications.To precisely formulate the tasks,the signal temporal logic(STL)framework is employed,where an auxiliary function is required to be designed based on the robust semantics of STL formulas.Considering the impact of input saturation,the proposed algorithm designs the auxiliary function in the form of cube power function,and incorporate it into the optimization problem in MPC.After that,the terminal ingredients are designed,whose parameters can be efficiently calculated based on linear matrix inequality techniques.Finally,numerical simulation is applied to validate the effectiveness of the proposed control strategy.展开更多
A method to model and analyze the hybrid systems is presented. The time to be considered in the plant is taken as an explicit parameter through the constrained predicated net (CPN). The CPN's basic structure is a ...A method to model and analyze the hybrid systems is presented. The time to be considered in the plant is taken as an explicit parameter through the constrained predicated net (CPN). The CPN's basic structure is a Petri net with predicated transition. All components of the net are expressed by annotation which is defined on rational set Q. The analysis method for the plant is interval temporal logic represented by Petri nets. This paper combines the above two methods to synthesize the hybrid system, gives a simple and clear expression of the expected action of the studied plant.展开更多
Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-terminat...Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-termination, and B (S), defining behaviour. Any two formulae A and B will define a corresponding program. Refinement is defined as implication between these formulae.展开更多
文摘The TLL XYZ/E is a formal language able to represent the dynamic semantics and the static semantics in a unified framework. It supports the whole process of program development, i.e. from the abstract specification to the efficiently executable program in a formal, precise and convenient way. The steam boiler control specification problem, a large case study in the fields of real time, hybrid and communication systems, is discussed with XYZ/E. The approach covers physical model construction, formal specification, stepwise refinement, verification, executable program and visual user interface programming.
基金supported by the National Natural Science Foundation of China under Grant 62173314.
文摘This paper investigates control synthesis for motion planning under conditions of uncertainty,specifically in robot motion and environmental properties,which are modeled using a probabilistic labeled Markov decision process(PL-MDP).To address this,a model-free reinforcement learning(RL)approach is designed to produce a finite-memory control policy that meets complex tasks specified by linear temporal logic(LTL)formulas.Recognizing the presence of uncertainties and potentially conflicting objectives,this study centers on addressing infeasible LTL specifications.A relaxed LTL constraint enables the agent to adapt its motion plan,allowing for partial satisfaction by accounting for necessary task violations.Additionally,a new automaton structure is introduced to increase the density of accepting rewards,facilitating deterministic policy outcomes.The proposed RL framework is rigorously analyzed and prioritizes two key objectives:(1)satisfying the acceptance condition of the relaxed product MDP,and(2)minimizing long-term violation costs.Simulation and experimental results are presented to demonstrate the framework’s effectiveness and robustness.
基金The National Natural Science Foundation of China (No.10974093)the Scientific Research Foundation for Senior Personnel of Jiangsu University (No.07JDG014)the Natural Science Foundation of Higher Education Institutions of Jiangsu Province (No.08KJD520015)
文摘In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system＇s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.
基金supported by National Natural Science Foundation of China under Grant No. 61003079
文摘Model checking based on linear temporal logic reduces the false negative rate of misuse detection.However,linear temporal logic formulae cannot be used to describe concurrent attacks and piecewise attacks.So there is still a high rate of false negatives in detecting these complex attack patterns.To solve this problem,we use interval temporal logic formulae to describe concurrent attacks and piecewise attacks.On this basis,we formalize a novel algorithm for intrusion detection based on model checking interval temporal logic.Compared with the method based on model checking linear temporal logic,the new algorithm can find unknown succinct attacks.The simulation results show that the new method can effectively reduce the false negative rate of concurrent attacks and piecewise attacks.
基金This work was partially supported by the National Natural Science Foundation of China(No.51475334)the National Key Research and Development Program of Science and Technology of China(No.2018YFB1305304)the Shanghai Science and Technology Pilot Project(No.19511132100).
文摘In this paper,w e provide a novel scheme to solve the motion planning problem of multi-agent systems under high-level task specifications.First,linear temporal logic is applied to express the global task specification.Then an efficient and decentralized algorithm is proposed to decom pose it into local tasks.M oreover,w e use control barrier function to synthesize the local controller for each agent under the linear temporal logic motion plan with safety constraint.Finally,simulation results show the effectiveness and efficiency of our proposed scheme.
基金The first author of this paper would like to thank the follow- ing scholars, Prof. Joseph Sifakis, 2007 Turing Award Winner, for his invaluable help with my research and Dr. Kevin Lu at Brunel University, UK for his excellent suggestions on this paper. This work was supported by the National Natural Sci- ence Foundation of China under Grant No.61003079 the Chi- na Postdoctoral Science Foundation under Grant No. 2012M511588.
文摘To combat the well-known state-space explosion problem in Prop ositional Linear T emp o- ral Logic （PLTL） model checking, a novel algo- rithm capable of translating PLTL formulas into Nondeterministic Automata （NA） in an efficient way is proposed. The algorithm firstly transforms PLTL formulas into their non-free forms, then it further translates the non-free formulas into their Normal Forms （NFs）, next constructs Normal Form Graphs （NFGs） for NF formulas, and it fi- nally transforms NFGs into the NA which ac- cepts both finite words and int-mite words. The experimental data show that the new algorithm re- duces the average number of nodes of target NA for a benchmark formula set and selected formulas in the literature, respectively. These results indi- cate that the PLTL model checking technique em- ploying the new algorithm generates a smaller state space in verification of concurrent systems.
基金Project supported by the National Natural Science Foundation of China （Grant Nos.60373072, 60673115）, the National Basic Research Program of China （Grant No.2002CB312001）, and the National High-Technology Research and Development Program of China （Grant No.2007AA012144）
文摘Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a fair timed automaton （TA） that recognizes its satisfying models with prototype verification system （PVS） in this paper. Both the tabular construction＇s principles and the PVS implementation details are given for the different type of MITL formula according to the corresponding semantics interpretations. After this transformation procedure, specifications expressed with MITL formula can be verified formally in the timed automata framework developed previously.
基金supported by the Fundamental Research Funds for the Central Universities(DUT22RT(3)090)the National Natural Science Foundation of China(61890920,61890921,62122016,08120003)Liaoning Science and Technology Program(2023JH2/101700361).
文摘Linear temporal logic(LTL)is an intuitive and expressive language to specify complex control tasks,and how to design an efficient control strategy for LTL specification is still a challenge.In this paper,we implement the dynamic quantization technique to propose a novel hierarchical control strategy for nonlinear control systems under LTL specifications.Based on the regions of interest involved in the LTL formula,an accepting path is derived first to provide a high-level solution for the controller synthesis problem.Second,we develop a dynamic quantization based approach to verify the realization of the accepting path.The realization verification results in the necessity of the controller design and a sequence of quantization regions for the controller design.Third,the techniques of dynamic quantization and abstraction-based control are combined together to establish the local-to-global control strategy.Both abstraction construction and controller design are local and dynamic,thereby resulting in the potential reduction of the computational complexity.Since each quantization region can be considered locally and individually,the proposed hierarchical mechanism is more efficient and can solve much larger problems than many existing methods.Finally,the proposed control strategy is illustrated via two examples from the path planning and tracking problems of mobile robots.
基金Supported by the National Natural Science Foundation of China (No.60603036)the Jiangsu Province Research Foundation (No.BK2007139)
文摘Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a guasi-classical temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. Our models are paraKripke structures (extended standard Kripke structures), in which both a formula and its negation are satisfied in a same state, and properties to be verified are expressed by QCTL with paraKripke structures semantics. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.
文摘The paper proposed an approach to study the power system voltage coordinated control using Linear Temporal Logic (LTL). First, the hybrid Automata model for power system voltage control was given, and a hierarchical coordinated voltage control framework was described in detail. In the hierarchical control structure, the high layer is the coordinated layer for global voltage control, and the low layer is the power system controlled. Then, the paper introduced the LTL language, its specification formula and basic method for control. In the high layer, global voltage coordinated control specification was defined by LTL specification formula. In order to implement system voltage coordinated control, the LTL specification formula was transformed into hybrid Automata model by the proposed algorithms. The hybrid Automata in high layer could coordinate the different distributed voltage controller, and have constituted a closed loop global voltage control system satisfied the LTL specification formula. Finally, a simple example of power system voltage control include the OLTC controller, the switched capacitor controller and the under-voltage shedding load controller was given for simulating analysis and verification by the proposed approach for power system coordinated voltage control. The results of simulation showed that the proposed method in the paper is feasible.
文摘Reachability-based analysis and temporal analysis are used to verify the properties of concurrent systems, and it is important to exploit fast and efficient methods. This paper gives semantics of temporal formulae with edges of the transition system of Petri net, and then presents a fast temporal analyzing method, which takes advantage of both Petri net and temporal logic. The method only expands a path of equivalence trace while the path does not satisfy a property according to trace semantics of Petri net, and can validate directly the property on Petri net. Moreover, we exploit a minimal degree of in-out of a node as heuristics to select a path of an equivalence trace. Finally, we demonstrate the validity of the method that decreases state spaces and improves the verification system with the experimental results.
基金supported in part by the National Science Foundation of China(Grant No.62333015),the Science Foundation of Shanghai(Grant No.24ZR1438800).
文摘The traffic rules governing the passage of different types of vehicles at signal-free intersections are distinct,especially for the emergency vehicles.Although these traffic rules can be described through deliberate mathematical expressions,but showing limitations in terms of the userfriendliness of rule description.This paper proposes an improved STL-based trajectory planning method for CAVs at signal-free intersections,describing traffic rules with STL formulas,which bridges the gap between human-understandable and machine-understandable traffic rules.The MPC framework is utilised to guarantee real-time trajectory planning by reducing travel time of vehicles passing through the intersection.Simulation results show improved traffic efficiency compared with other methods while ensuring adherence to yielding rules for emergency CAVs.
基金supported in part by the National Natural Science Foundation of China under Grant No.62103275.
文摘This paper proposes a model predictive control(MPC)algorithm for a small satellite to accomplish on-orbit inspection missions.The relative dynamics of satellite is modelled first.Then,multiple constraints are taken into account for the on-orbit inspection missions,including input saturation,obstacle avoidance,velocity limit,and task specifications.To precisely formulate the tasks,the signal temporal logic(STL)framework is employed,where an auxiliary function is required to be designed based on the robust semantics of STL formulas.Considering the impact of input saturation,the proposed algorithm designs the auxiliary function in the form of cube power function,and incorporate it into the optimization problem in MPC.After that,the terminal ingredients are designed,whose parameters can be efficiently calculated based on linear matrix inequality techniques.Finally,numerical simulation is applied to validate the effectiveness of the proposed control strategy.
文摘A method to model and analyze the hybrid systems is presented. The time to be considered in the plant is taken as an explicit parameter through the constrained predicated net (CPN). The CPN's basic structure is a Petri net with predicated transition. All components of the net are expressed by annotation which is defined on rational set Q. The analysis method for the plant is interval temporal logic represented by Petri nets. This paper combines the above two methods to synthesize the hybrid system, gives a simple and clear expression of the expected action of the studied plant.
文摘Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-termination, and B (S), defining behaviour. Any two formulae A and B will define a corresponding program. Refinement is defined as implication between these formulae.
