新书推介：《语义网技术体系》
作者：瞿裕忠，胡伟，程龚
   XML论坛     >>W3CHINA.ORG讨论区<<     计算机科学论坛     SOAChina论坛     Blog     开放翻译计划     新浪微博  
 
  • 首页
  • 登录
  • 注册
  • 软件下载
  • 资料下载
  • 核心成员
  • 帮助
    		•   Add to Google

    >> It is the theory that decides what can be observed. - Albert Einstein
    [返回] W3CHINA.ORG讨论区 - 语义网·描述逻辑·本体·RDF·OWL → 计算机理论与工程 → 『 理论计算机科学 』 → 这里有没有做Model Checking的？ ◇查看新帖 ◇ 用户列表 ◇

      发表一个新主题  发表一个新投票  回复主题  (订阅本版) 您是本帖的第 44095 个阅读者浏览上一篇主题  刷新本主题   树形显示贴子　浏览下一篇主题
     * 贴子主题： 这里有没有做Model Checking的？ 举报  打印  推荐  IE收藏夹 
       本主题类别:     
     copperccnu 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：6
      积分：84
      门派：XML.ORG.CN
      注册：2005/3/12

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给copperccnu发送一个短消息 把copperccnu加入好友 查看copperccnu的个人资料 搜索copperccnu在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看copperccnu的博客楼主
    发贴心情 这里有没有做Model Checking的？

    最近在看CTL*的东西，可是自己一举个例子来验证，就发现自己还没有真正搞懂。
    这里有没有过来人，指点一二。

       收藏   分享  
    顶(0)
      




    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/3/29 19:47:00
     
     blackxv 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：3
      积分：69
      门派：XML.ORG.CN
      注册：2005/3/29

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给blackxv发送一个短消息 把blackxv加入好友 查看blackxv的个人资料 搜索blackxv在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看blackxv的博客第2楼
    发贴心情 
    CTL＊　＝　LTL　＋CTL
    应该先弄明白路径公式和状态公式的特征
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/3/29 19:57:00
     
     GaloisAbel 美女呀，离线，快来找我吧！
      
      
      等级：大一新生
      文章：4
      积分：101
      门派：XML.ORG.CN
      注册：2005/3/16

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给GaloisAbel发送一个短消息 把GaloisAbel加入好友 查看GaloisAbel的个人资料 搜索GaloisAbel在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看GaloisAbel的博客第3楼
    发贴心情 
    handbook of theoretical computer science
    semantics的那个volume (好像是B)是蛮精辟的解释
    cs类的不少书都有仔细专门的解释

    clark那本经典的model checking有提

    时序逻辑ms蛮直观

    嗯，model checking算上偶吧，先
    偶正在theorem proving混，郁闷中！
    希望能结合了model checking来弄

    顺便问问，你是作hardware circuit 还是software verification 或其它什么

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/3/30 0:49:00
     
     copperccnu 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：6
      积分：84
      门派：XML.ORG.CN
      注册：2005/3/12

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给copperccnu发送一个短消息 把copperccnu加入好友 查看copperccnu的个人资料 搜索copperccnu在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看copperccnu的博客第4楼
    发贴心情 
    path formulae 和state formulae我想我还是搞明白了的。
    也许是还没学会走就想跑吧。

    做software verification，
    MIT99年的那本Model Checking感觉象是很多论文的集合，
    讲的不是很细致，不知道是否适合作为入门级的。

    上学期在学习做Slicing，这学期开始Model Checking，正琢磨着是不是能够用切片结合模型验证来提高验证算法的效率，或者是缓解以下状态空间爆炸也好。

    我的数理逻辑知识不好，定理证明对我很困难的。好像看到过有将这二者结合起来做的文章。

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/3/30 16:24:00
     
     yangfeather 帅哥哟，离线，有人找我吗？
      
      
      等级：大一(高数修炼中)
      文章：10
      积分：110
      门派：XML.ORG.CN
      注册：2005/3/12

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给yangfeather发送一个短消息 把yangfeather加入好友 查看yangfeather的个人资料 搜索yangfeather在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看yangfeather的博客第5楼
    发贴心情 
    那本model checking的书还是蛮好的吧！我们这边是在用这本书开讨论班!你如果是在北京的话,可以过来参加!
    确实可以用切片的方法结合模型检测来提高算法的效率
    CTL＊　＝　LTL　＋CTL  好像不能这么简单的相加和相等
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/3/30 17:11:00
     
     shimutou 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：3
      积分：73
      门派：XML.ORG.CN
      注册：2005/3/31

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给shimutou发送一个短消息 把shimutou加入好友 查看shimutou的个人资料 搜索shimutou在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看shimutou的博客第6楼
    发贴心情 
    clarke 那本书很好的，要慢慢读。我花了大半年时间才读完。
    有问题我们可以切磋，我的油箱：chzhou@mail.edu.cn
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/3/31 16:32:00
     
     pjwhu 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：0
      积分：62
      门派：XML.ORG.CN
      注册：2005/3/16

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给pjwhu发送一个短消息 把pjwhu加入好友 查看pjwhu的个人资料 搜索pjwhu在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看pjwhu的博客第7楼
    发贴心情 
    请问copperccnu有 Model Checking,E.M.Clarke 的书吗?
    能借我复印一下吗?
    我在武汉:)
    谢谢了
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/4/1 20:28:00
     
     shenhaozr 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：2
      积分：89
      门派：XML.ORG.CN
      注册：2005/3/14

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给shenhaozr发送一个短消息 把shenhaozr加入好友 查看shenhaozr的个人资料 搜索shenhaozr在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看shenhaozr的博客第8楼
    发贴心情 model checking general
    模型检查（ 无限模型->有限模型）

    模型
    规范
    实现

    Model |= Logic
         Satisfy


    实现 |= 规范
         计算

    逻辑 ...
    自动机 ...
    进程代数 ...
    博弈...
    ...

    计算复杂性与描述复杂性关系

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/4/4 12:53:00
     
     yangfeather 帅哥哟，离线，有人找我吗？
      
      
      等级：大一(高数修炼中)
      文章：10
      积分：110
      门派：XML.ORG.CN
      注册：2005/3/12

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给yangfeather发送一个短消息 把yangfeather加入好友 查看yangfeather的个人资料 搜索yangfeather在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看yangfeather的博客第9楼
    发贴心情 
    关于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也有被运用，尤其是在使用自动机来识别图时。
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/4/5 0:33:00
     
     yangfeather 帅哥哟，离线，有人找我吗？
      
      
      等级：大一(高数修炼中)
      文章：10
      积分：110
      门派：XML.ORG.CN
      注册：2005/3/12

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给yangfeather发送一个短消息 把yangfeather加入好友 查看yangfeather的个人资料 搜索yangfeather在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看yangfeather的博客第10楼
    发贴心情 
    关于进程代数：
    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统一
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2005/4/5 1:47:00
     
     GoogleAdSense
      
      
      等级：大一新生
      文章：1
      积分：50
      门派：无门无派
      院校：未填写
      注册：2007-01-01
    给Google AdSense发送一个短消息 把Google AdSense加入好友 查看Google AdSense的个人资料 搜索Google AdSense在『 理论计算机科学 』的所有贴子 访问Google AdSense的主页 引用回复这个贴子 回复这个贴子 查看Google AdSense的博客广告
    2025/2/18 15:30:51

    本主题贴数24，分页： [1] [2] [3]

    管理选项： 修改tag | 锁定 | 解锁 | 提升 | 删除 | 移动 | 固顶 | 总固顶 | 奖励 | 惩罚 | 发布公告
    W3C Contributing Supporter! W 3 C h i n a ( since 2003 ) 旗 下 站 点
    苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
    		 5,875.000ms