[1] Zhou Lianke.Research on traffic flow density based broadcasting technologies in VANETS[D].Harbin Institute of Technology,2011.
[2] Biswas S,Tatchikou R,Dion F.Vehicle-to-vehicle wireless communication protocols for enhancing highway traffic safety[J].IEEE Communications Magazine,2006,44(1):74-82.
[3] Sproston J.Discrete-time verification and control for probabilistic rectangular hybrid automata[A].Proc 8th Int Conf Quantitative Evaluation of SysTems (QEST'11)[C].Aachen,Germany,2011,79-88.
[4] Chatterjee,K.Markov decision processes with multiple long-run average objectives[A].Proc 27th Int Conf on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07)[C].Springer,2007,473-484.
[5] Kwiatkowska M,Norman G,Segala R,Sproston J.Verifying quantitative properties of continuous probabilistic timed automata[A].Proc 11th Int Conf of Concurrency Theory(CONCUR 2000)[C].PA,USA,Springer,2000,123-137.
[6] 刘志锋,孙博,周从华.概率实时时态认知逻辑模型检测中抽象技术的研究[J].电子学报,2013,41(7):1343-1351. Liu Zhi-feng,Sun Bo,Zhou Cong-hua.Abstuaction in model checking probabilistic real-time temporal logic of knowledge[J].Acta Electronica Sinica,2013,41(7):1343-1351.(in Chinese)
[8] Norman G,Parker D,Sproston J.Model checking for probabilistic timed automata[J].Formal Methods in System Design,2013,43(2):164-190.
[9] Taolue Chen,Jian Lu.Probabilistic alternating-time temporal logic and model checking algorithm[A].Proc 4th Int Conf on Fuzzy Systems and Knowledge Discovery( FSKD 2007)[C].Haikou:IEEE,2007.35-39.
[10] Kwiatkowska M,Norman G,Parker D.PRISM 4.0:Verification of Probabilistic Real-time Systems[A].Proc 23rd Int Conf on Computer Aided Verification (CAV'11)[C].UT, USA:Springer,2011.585-591.
[11] 刘鸿飞.VANET信息广播模型与优化方法研究[D].重庆大学,2009. |