|
以文本方式查看主题 - 计算机科学论坛 (http://bbs.xml.org.cn/index.asp) -- 『 理论计算机科学 』 (http://bbs.xml.org.cn/list.asp?boardid=64) ---- 这里有没有做Model Checking的？ (http://bbs.xml.org.cn/dispbbs.asp?boardid=64&rootid=&id=16210) |
|
-- 作者：copperccnu -- 发布时间：3/29/2005 7:47:00 PM -- 这里有没有做Model Checking的？ 最近在看CTL*的东西，可是自己一举个例子来验证，就发现自己还没有真正搞懂。 这里有没有过来人，指点一二。 |
|
-- 作者：blackxv -- 发布时间：3/29/2005 7:57:00 PM -- CTL＊ ＝ LTL ＋CTL 应该先弄明白路径公式和状态公式的特征 |
|
-- 作者：GaloisAbel -- 发布时间：3/30/2005 12:49:00 AM -- handbook of theoretical computer science semantics的那个volume (好像是B)是蛮精辟的解释 cs类的不少书都有仔细专门的解释 clark那本经典的model checking有提 时序逻辑ms蛮直观 嗯，model checking算上偶吧，先 顺便问问，你是作hardware circuit 还是software verification 或其它什么 |
|
-- 作者：copperccnu -- 发布时间：3/30/2005 4:24:00 PM -- path formulae 和state formulae我想我还是搞明白了的。 也许是还没学会走就想跑吧。 做software verification， 上学期在学习做Slicing，这学期开始Model Checking，正琢磨着是不是能够用切片结合模型验证来提高验证算法的效率，或者是缓解以下状态空间爆炸也好。 我的数理逻辑知识不好，定理证明对我很困难的。好像看到过有将这二者结合起来做的文章。 |
|
-- 作者：yangfeather -- 发布时间：3/30/2005 5:11:00 PM -- 那本model checking的书还是蛮好的吧！我们这边是在用这本书开讨论班!你如果是在北京的话,可以过来参加! 确实可以用切片的方法结合模型检测来提高算法的效率 CTL＊ ＝ LTL ＋CTL 好像不能这么简单的相加和相等 |
|
-- 作者：shimutou -- 发布时间：3/31/2005 4:32:00 PM -- clarke 那本书很好的，要慢慢读。我花了大半年时间才读完。 有问题我们可以切磋，我的油箱：chzhou@mail.edu.cn |
|
-- 作者：pjwhu -- 发布时间：4/1/2005 8:28:00 PM -- 请问copperccnu有 Model Checking,E.M.Clarke 的书吗? 能借我复印一下吗? 我在武汉:) 谢谢了 |
|
-- 作者：shenhaozr -- 发布时间：4/4/2005 12:53:00 PM -- model checking general 模型检查（ 无限模型->有限模型） 模型 Model |= Logic 逻辑 ... 计算复杂性与描述复杂性关系
|
|
-- 作者：yangfeather -- 发布时间：4/5/2005 12:33:00 AM -- 关于model checking: 1. 在模型检测中，我们关注的往往是local property，而不是global property，所以使用时序逻辑，模态mu演算等等，而不是使用一阶逻辑或者二阶逻辑，当然前者与后者有一定的关系，具体的关系，可以学习一下关于modal logic的一些知识，在modal logic的框架内看这些问题，就能很清晰。 2. 在model checking中，还是有很多的理论问题可以做的，比如LTL的模型检测中，Buchi自动机的求补问题，如何提高效率；modal mu calculus中多个不动点嵌套的公式的模型检测问题；时序逻辑，modal mu caluclus的描述能力的问题，这些问题都是非常难得，说实在的，就国内研究的水平来说，做这些问题，还是比较困难的，风险也比较大(弄不好，就毕不了业）。 3.在model checking的理论研究中，尤其是在研究逻辑的描述能力的问题中，自动机是一个比较主要的工具，game theory也有被运用，尤其是在使用自动机来识别图时。
|
|
-- 作者：yangfeather -- 发布时间：4/5/2005 1:47:00 AM -- 关于进程代数： 1. 进程代数最初主要是关注系统之间的相等关系，比如CCS中的strong/weak bisimulation equivalence, CSP中的failure equivalence等等；后来model checking出现后，也有人拿它来做model chekcing，这时将进程表达式看作一个程序，然后检测它是否满足某个用一定的逻辑描述的性质，用的比较多的逻辑是modal mu caluclus； 2.早期的进程代数只有进程之间的简单同步，在计算过程中，进程之间的通信拓扑不发生变化；进程代数进一步的发展，出现了在计算过程中通信拓扑可以发生变化的pi calculus，对于pi calculus, 发展了它的关于相等的理论，同时也引入了相应的逻辑，比如first order modal mu culculus,可以做model checking，此外，还可以使用所谓的type system来帮助保证正确性;这样，相等理论，引入逻辑作model checking,利用type system，这三点成为许多进程演算理论的三个方面。 3. 关于进程代数中的model checking问题，在后来出现的异步pi calculus，以及mobile ambient中，由于采用了类似term rewriting的方式来做语义，引入的逻辑不仅可以描述时序性质，还可以描述空间信息。 4. 现在进程代数的发展是多方向的，有关于real time system, hybrid system的进程代数，有带有概率信息的进程代数，有前面提到的关于移动计算的pi caluclus和mobile ambient 5.在国内做进程代数的人当中，中科院软件所的林惠民院士的工作是在国际上影响最大的，他和Hennesy共同提出的symbolic bisimulation，在传值的进程代数和pi calculus中，都有非常好的应用；中科院软件所的柳欣欣研究员，也作了不少很有影响的工作，比如，solving equation of CCS，使用 pi calculus 作面向对象程序设计语言的语义，modal mu calculus中fixpoint alternation free公式得多项式时间的模型检测算法；清华的应明生教授，用拓扑作进程代数的语义；上海交大的傅玉熙教授提出的chi calculus 6.4月11-20，进程代数领域的central person Robin Milner(Turing Award)将访问中科院软件所，其间他将介绍他最新发展的一个基础框架，可以将许多进程代数，甚至lambda calculus，petri net统一
|
|
-- 作者：ljb -- 发布时间：4/5/2005 9:19:00 AM -- “尤其是在使用自动机来识别图时。” 这个东西哪里有介绍？？
|
|
-- 作者：copperccnu -- 发布时间：4/5/2005 8:05:00 PM -- 武大的同学，书不在我手上，不好意思啊。网上可以找到一些论文，CMU有几个TR可以下载来看，都是以前的PhD Thesis。 最近在看将LTL公式转换成Buchi自动机后如何约简自动机提高效率的文章。yangfeather，你提到的Buchi自动机求补问题，的确还没有认真想过。 |
|
-- 作者：zhaoming -- 发布时间：4/22/2005 7:00:00 PM -- 以前看到一本书<model checking>,翻了一下,挺好,没细看, 在做automata,涉及到TCTL和STCTL,觉得这方面面太广,一个人能做的太有限, 可选的题目太多太多. |
|
-- 作者：twosteps -- 发布时间：8/1/2005 8:59:00 AM -- 举个小手， 偶的毕业论文大方向就是这个， 我是在国外念的大学，很想以后回国工作，不过今天浏览了这个论坛后，发现很多专业词中文都不知道，只能马马乎乎的瞎猜。。。以后还要多请教各位大侠。 上面提到的那个 buchi automaton 求 complement 的问题，印象中是要分情况讨论的，也就是 deterministic 和 nondeterministic， 因为 deterministic buchi automata 比较 weak, 而nondeterministic buchi automata 和 muller, rabin, parity 是equivalent 的。也可能说的不对，以前学的，考完就忘了。。。 |
|
-- 作者：twosteps -- 发布时间：8/1/2005 9:04:00 AM -- 偶以前学过自动机识别二维图，实际上识别的就是识别一个数组。不知道是不是你想问的。 |
|
-- 作者：fq4731 -- 发布时间：8/12/2005 3:25:00 PM -- 有研究进程代数和pi演算进行模型验证的吗？ 有的话可以讨论讨论哦 QQ：361169937 |
|
-- 作者：skatingon -- 发布时间：8/14/2005 8:40:00 PM -- 我在做Isabelle/Isar，有没有同学也做这个？skatingon@gmail.com |
|
-- 作者：royzy -- 发布时间：8/25/2005 3:10:00 PM -- 偶今年刚上研一，对这个形式化验证的东西不太了解，我想请教一些问题，如果要把这个模型检测和实际的东西结合起来的话，除了Spin.STeP这样的东西外，还能从哪方面着手呀？？ |
|
-- 作者：hgawu -- 发布时间：3/25/2006 5:11:00 PM -- 这位老兄说的好，不知道是何方神圣？我也是做进程代数的。交流交流如何？ |
|
-- 作者：sosoid -- 发布时间：3/30/2006 9:48:00 AM -- 瞎逛逛到这里了 原来有这么多人做model checking的 我刚上研 这些方面刚看了两本书 1 面向计算机科学的数理逻辑（影印，不是陆老师那本） 2 3 以后来这边和大家多交流 呵呵
|
|
-- 作者：linrd -- 发布时间：4/3/2006 5:30:00 PM -- 应该多多交流，尤其是资料方面 |
|
-- 作者：linrd -- 发布时间：4/3/2006 11:05:00 PM -- 可以将SPIN model checker作简单评论吗？
|
|
-- 作者：mqznudt -- 发布时间：4/6/2006 11:32:00 PM -- 现在正在学习NASA关于LIVINGSTONE的东西,谁知道这些,请赐教! |
|
-- 作者：dustion -- 发布时间：4/16/2006 10:31:00 PM -- 太好了，请问一下各位有研究 agent communication 的吗？ 我的研究方向是agent & mas 的 ACL语义研究。 |
|
W 3 C h i n a ( since 2003 ) 旗 下 站 点 苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》 |
6,562.500ms |