Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more
3 votes

Can CTL* express every model's behaviour

First of all, for every transition system M, there indeed exists a CTL* formula Φ such that M ⊨ Φ holds, namely the CTL* formula "true". What you may have wanted to express is the question ...
DCTLib's user avatar
  • 2,787
2 votes

Is there a linear programming method that is polynomial in the number of variables, constraints and bitlength of numbers?

Interior-point methods such as Khachiyan’s and Karmarkar’s are, indeed, polynomial in the size of the input, i.e., in the number of variables, constraints, and the bitlength of the coeficients. This ...
Emil Jeřábek's user avatar
2 votes

Can remainder mod 2 be efficiently computed from addition and equality?

I really like this question! Here's a sketchy argument for a negative answer (as expected) which I think works but may need some details filled in: Suppose our putative polytime parity-checking ...
Noah Schweber's user avatar
1 vote

Linear Time properties classification

As Wikipedia says, not every property is a safety property or a liveness property (consider "a occurs exactly once") The parenthetical gives an example of a property that is not a safety ...
D.W.'s user avatar
  • 160k

Only top scored, non community-wiki answers of a minimum length are eligible