Model checking with CTL

From: Huy Lam (lamhuy_at_vt.edu)
Date: Wed Mar 21 2007 - 16:41:43 MDT

• Next message: Fabio Somenzi: "Re: Model checking with CTL"
• Previous message: Mike Lyon: "POTENTIAL SPAM: Melt away fat easily"
• Next in thread: Fabio Somenzi: "Re: Model checking with CTL"
• Reply: Fabio Somenzi: "Re: Model checking with CTL"
• Reply: Fabio Somenzi: "Re: Model checking with CTL"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

To whom this may concern:

My name is Jason. I am currently a graduate student at Virginia Tech. I have
been trying to use VIS model_checking commands to verify a few properties
such as reachablity: EF(p). If I like to specify an initial state S0:

S0 |= EF(p)

How do that write that ctl formula so VIS can perform the checking. Does VIS
prefer EF command or AG

Thank you for any help

Jason

• Next message: Fabio Somenzi: "Re: Model checking with CTL"
• Previous message: Mike Lyon: "POTENTIAL SPAM: Melt away fat easily"
• Next in thread: Fabio Somenzi: "Re: Model checking with CTL"
• Reply: Fabio Somenzi: "Re: Model checking with CTL"
• Reply: Fabio Somenzi: "Re: Model checking with CTL"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

This archive was generated by hypermail 2.1.7 : Wed Mar 21 2007 - 16:43:40 MDT