I have read a bit about the different logics a while ago but I am not an expert in them. I remember reading somewhere something about functions in logic having some issues as opposed to basic propositions or predicates or something like that. This answer also suggests, at least in programming, there is something different about functions when it comes to logical operations.
I have also read a little about Binary Decision Diagrams (BDD) and MDD's used to represent Boolean functions, and decision trees. Since BDDs are just essentially Boolean functions, they can be used in formal verification, though I am not too sure how to apply it yet. Yet, all of these use examples of pretty much synchronous or highly abstracted logical functions, where seemingly every nested function in the logical formula "evaluates" at once, so is synchronous. You don't even consider how it evaluates like you would in programming, it either resolves to true or false.
But all of this has had me wondering about what if you actually considered the evaluation of the functions. If this were an Assembly-evaluating computer, then each logical operation would be one "step" in the program, store its value output somewhere (which itself is taking time on the circuit board), etc.. Until finally the logical formula resolves.
Take this a little further and say you have functions that are really asynchronous. That is, something like this:
A(B, C(D, E(F, G))) & C(B, G) & !D & !E(F, B)
Just using something that might be complex. Say that the E(F, G) function was asynchronous. That is, maybe it is a check that a remote file from the cloud exists. Then it has a lot of background stuff that it does inherently. Maybe even it has unintended side effects that could influence the outcome of C(B, G). So assuming we figure out the order that things need to evaluate in, I am interested in trying to "formally reason about about this system". We have basically an asynchronously evaluating BDD (assuming we convert the logical formulas to one), and there is some sequencing that happens in the evaluation of the functions so that they resolve correctly and handle the asyncness.
Basically my question is, the area of math that can formally reason about such a system. Where you can write some logical formulas, yet those formulas can be highly asynchronous with side effects, and yet still the logical formula can be used in proofs of some sort. I have seen Sequential logic and Asynchronous logic, but they both don't seem to be too math heavy or about formal proofs. I am looking for something that can allow you to do formal proofs with some sort of logic of asynchronous stuff, some of which are async logical formulas themselves. I have also seen the Temporal logic of actions, but not sure if that is it.
But then there is Concurrency and Distributed Systems, Petri Nets, and stuff like that. However, this is different than logic I think.
To summarize, I am looking for some way of being able to reason about asynchronous logical functions. Because there is realistically no way a logical formula can all evaluate all at once, there is inherently (physically) asynchronicity in the evaluation of the functions, and I want to take that into account. And I would like to be able to use this for formally verifying systems.