%0 Journal Article
%T Hybrid Projection Temporal Logic and Formal Verifications of Hybrid Systems<br>混合投影时序逻辑与混合系统的形式化验证
%A ZHANG Hai-Bin
%A DUAN Zhen-Hua
%A <br>张海宾
%A 段振华
%J 计算机科学
%D 2007
%I 
%X To describe properties of hybrid systems, many temporal logics such as Hybrid Temporal Logic have been formalized. Although being good at describing properties of hybrid systems, these logics are not suitable for describing the behaviors of such systems. In this paper, a hybrid projection temporal logic (HPTL) is formalized. It can be used to describe both properties and implementations of hybrid systems, which enables us to do verifications of hybrid sys- tems over the same mathematical model. In addition, a set of logical equivalent formulas and an example of verifications using HPTL are given.
%K Hybrid systems
%K Hybrid automata
%K Interval temporal logic
%K Formal verification<br>混合系统
%K 混合自动机
%K 区间时序逻辑
%K 形式化验证
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=E6B09177B3CCFB7FA3B7769EFBF73439&yid=A732AF04DDA03BB3&vid=339D79302DF62549&iid=708DD6B15D2464E8&sid=69E4C201C13601F9&eid=4133DDB79B497495&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=8