Alloy Community

User login
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 25.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 26.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 27.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 28.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 29.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 30.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 31.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 32.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 33.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 34.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 25.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 26.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 27.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 28.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 29.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 30.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 31.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 32.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 33.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 34.

ca we expresse CTL?

Home » Forums » Other » I don't know where to post this
 
Posted on: Thu, 01/21/2010 - 22:08
med
Joined: 2009-10-02
Points: 73
User is offline
ca we expresse CTL?
Hi,
I have a problem,i have to  say something like this " theres is  always a way to leave the Library when you are a member" ,the problem is that in my model and in LTL we can not say "there is always a way" ,so i decide to construct a transition graph that it allowed me to express this proprieties ,but i have another problem is the limit of atoms that it will generate...
so if we have any idea,or there is some one who has the same problem,I am a customer :)
Thanks
 
Posted on: Thu, 01/21/2010 - 22:22    #1
Felix Chang
Joined: 2008-05-15
Points: 377
User is offline
SAT solvers cannot solve arbitrary CTL problems. Certain CTL problems can be translated into equisatisfiable LTL problems, but not all. (Please consult various classical textbooks on how to determine if a particular CTL problem is also LTL)

Syndicate content  

The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.

Theme originally designed by Chris Herberte