Model checking involves a process we call state transition. In Tau the GSSOTC is the temporal logic which allows for creation of a specification which gives a detailed map of how this state transition is supposed to happen. According to documentation Tau Language using GSSOTC is capable of not just sequential, but also tree based input.
Finite States
Most smart contracts can be represented as a finite state machine. For example an escrow contract can be thought of as a finite state machine. There is the initial state where both parties make their deposits, and there is also a final state where both sides are satisfied with their transactions. There are a finite number of possible states the smart contract can be in, and all of these possible states can be mapped. When it's done in the form of a formal specification, there are absolute security guarantees, there are a fixed number of possible states or positions on the map, and no additional positions are ever possible, so all behavior from the smart contract or application are apparent. Another way of saying this is formal verification is the process of checking mathematically that the behavior of the smart contract or application is exactly as specified. There are no bugs, no hidden states, no unknowns, it does exactly as specified.
For example a Rubiks cube can be represented as a constraint satisfiability problem. A Rubik's cube has finite states. 43,252,003,274,489,856,000 possible states to be exact. The problem can be abstracted, mapped into a Tau Language formula, and solved.
Complexity Class and Input Size
In Tau Language you can specify a program using a logic formula. A logic formula can have varying levels of complexity, but we know the complexity classes. It is known when a complexity class is exponential or beyond the problem of state explosion becomes apparent. The two variable fragment with counting has complexity class NEXPTIME-complete. This complexity is higher than NP, but lower than the complexity of full first-order logic, which is undecidable. While NEXPTIME-complete problems are theoretically solvable, they are generally considered intractable for large inputs.
State explosion
The larger the input size, the more variables and complexity in your formula, the greater the potential for state explosion. The growth of possible states of the smart contract or program is exponential, and at some point it will become computationally infeasible. Where that point is, for practical purposes, I don't know, and I'm not sure anyone knows yet. The way to find out is to try big formulas, big inputs, and see how Tau handles it. Theoretically we can predict state explosion, but depending on how Tau handles it, it might be manageable.
Some problems will be solved in miliseconds usings a desktop CPU and less than 64 gigs of ram. Other problems might take minutes to hours and require terabytes or more of ram with lots of CPUs. Agoras will have utility because it can be mathematically estimated how much it will cost in computational resources to do certain kinds of apps or certain formulas, so I can say computation resources will be in tremendous demand. If the average person has only 64 gigs of ram and an ordinary CPU, to really use some truly sophisticated smart contracts, the demand will be for lots and lots of CPUs, with lots and lots of ram. Agoras will be able to satisfy the demand, at least in theory, and in likelihood it will be companies setting up data centers who offer subscription (payable in Agoras or USD).
I will discuss this more at a later date but the state explosion problem can be mitigated by managing the input size (formula size) or by managing memory/CPU resources.