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.展开更多
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.展开更多
In the paper,we investigate the problem of finding a piecewise output feedback control law for an uncertain affine system such that the resulting closed-loop output satisfies a desired linear temporal logic (LTL) spec...In the paper,we investigate the problem of finding a piecewise output feedback control law for an uncertain affine system such that the resulting closed-loop output satisfies a desired linear temporal logic (LTL) specification.A two-level hierarchical approach is proposed to solve the problem in a triangularized output space.In the lower level,we explore whether there exists a robust output feedback control law to make the output starting in a simplex either remains in it or leaves via a specific facet.In the higher level,for the triangularization,we construct the transition system according to the reachability relationship obtained in the lower level and search for feasible paths that meet the LTL specification.The control approach is then applied to solve a motion planning problem.展开更多
Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although...Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.展开更多
The construction of B0chi automata from linear temporal logic is a significant step in model checking. This paper presents a depth-first constr,uction algorithm to obtain simple B0chi automata from linear-time tempora...The construction of B0chi automata from linear temporal logic is a significant step in model checking. This paper presents a depth-first constr,uction algorithm to obtain simple B0chi automata from linear-time temporal logic which significantly reduces the sizes of the state spaces. A form-filling algorithm was used to reduce the size of the generated automata and the algorithms were applied directly to state-based Buchi automata, without transformation into transition-based automata. A form-filling algorithm for the Buchi automata, which is based on the form-filling algorithm for deterministic automata, was developed by redefining parts of the configuration of the Buchi automata as well as the transition function. The correctness of this form-filling algorithm was proven. Tests show that this approach is competitive, especially on LTL formulae in the form of G, F, and U.展开更多
An abstraction method developed for the explicit linear temporal logic model checking was geared towards reducing the useless part of the state space during the abstraction period. This reduces the cost during the abs...An abstraction method developed for the explicit linear temporal logic model checking was geared towards reducing the useless part of the state space during the abstraction period. This reduces the cost during the abstraction period relative to models requiring many useless states. A dining-philosophers example comparing this abstraction method with conventional methods indicates that a large proportion of the state space has been reduced by this abstraction method. Finally, the abstract method is shown to be correct and an analysis is given to show how such a large proportion of states can be reduced.展开更多
In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs i...In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research. A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software. Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method＇s effectiveness. Linear temporal logic was used to model an interdomain routing system and its properties were analyzed. An example is included to demon- strate the method＇s reliability.展开更多
基金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.
基金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.
基金sponsored by the Scientific Research Foundation for the Returned Overseas Chinese Scholars,State Education Ministry of China
文摘In the paper,we investigate the problem of finding a piecewise output feedback control law for an uncertain affine system such that the resulting closed-loop output satisfies a desired linear temporal logic (LTL) specification.A two-level hierarchical approach is proposed to solve the problem in a triangularized output space.In the lower level,we explore whether there exists a robust output feedback control law to make the output starting in a simplex either remains in it or leaves via a specific facet.In the higher level,for the triangularization,we construct the transition system according to the reachability relationship obtained in the lower level and search for feasible paths that meet the LTL specification.The control approach is then applied to solve a motion planning problem.
文摘Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.
基金Supported by the National Natural Science Foundation of China(No. 60635020)the Basic Research Foundation of Tsinghua National Laboratory for Information Science and Technology(TNList)the Foundation of Japan Society for the Promotion of Science
文摘The construction of B0chi automata from linear temporal logic is a significant step in model checking. This paper presents a depth-first constr,uction algorithm to obtain simple B0chi automata from linear-time temporal logic which significantly reduces the sizes of the state spaces. A form-filling algorithm was used to reduce the size of the generated automata and the algorithms were applied directly to state-based Buchi automata, without transformation into transition-based automata. A form-filling algorithm for the Buchi automata, which is based on the form-filling algorithm for deterministic automata, was developed by redefining parts of the configuration of the Buchi automata as well as the transition function. The correctness of this form-filling algorithm was proven. Tests show that this approach is competitive, especially on LTL formulae in the form of G, F, and U.
基金Supported by the National Natural Science Foundation of China(No. 60635020)the Basic Research Foundation of Tsinghua National Laboratory for Information Science and Technology(TNList)
文摘An abstraction method developed for the explicit linear temporal logic model checking was geared towards reducing the useless part of the state space during the abstraction period. This reduces the cost during the abstraction period relative to models requiring many useless states. A dining-philosophers example comparing this abstraction method with conventional methods indicates that a large proportion of the state space has been reduced by this abstraction method. Finally, the abstract method is shown to be correct and an analysis is given to show how such a large proportion of states can be reduced.
基金Supported by the Basic Research Foundation of Tsinghua National Laboratory for Information and Technology (TNList)the JSPS Foundation
文摘In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research. A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software. Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method＇s effectiveness. Linear temporal logic was used to model an interdomain routing system and its properties were analyzed. An example is included to demon- strate the method＇s reliability.
