Formalizing the Virus Exposure Problem

As much of world is practicing “social distancing” or some version of it, I would venture to guess that many are getting “cabin fever” from the extended isolation. For me this condition has led to a blurred line between work and home and more interestingly news coverage and formal applications.

For example, the concept of social distancing and having small networks or circles of contact is aimed to reduce exposure to the virus. While probabilistically, the benefits are undeniable, a question that many of us have is whether we will be exposed to the virus given the precautions we are taking?

The analogy of this question in the formal domain fits the famous “reachability” problem. Let’s structure the question in a slightly more formalized way:

 Given the set of infected people P, does there exist a path (through people) from P to me?

To get the answer with formal, you would build the network/circles of contacts and do a reachability analysis from all the sources P  to the destination, me. This seems like a good application for a Connectivity Checking application where the source and destination are easily defined. Or if you think of the sources are initial states and the destination as a cover statement in SVA, then it would fit the Formal Property Verification (FPV) application. Or if the destination is considered a code coverage target, the Formal Coverage Analyzer (FCA) application would do the trick.

If we leave the problem as-is, the answer to our question is most likely “Yes” for most people. Consider the exposure from all the infected people through their circles and contact through the places they have visited (such as grocery stores, hospitals) or personal at essential businesses. For the answer to be “No”, you would have to either be amazingly well isolated OR take great precautions (masks, gloves, sanitizing objects before contact, etc.). Those two approaches would either break the path to your circle (structurally disconnected in circuit) or block any propagation into your circle (imagine a AND gate with one input set to 0).

There is another way to adjust the problem to be more realistic and that is to bound the infection propagation to timeline. Formally, we could try the following:

Given the set of infected people P, does there exist a path (through people) from P to me, in N days?

Now, we are asking whether the infected people P can expose enough other people that within N days it would have reached me. Depending on the number of people in your circle and what activities you have been engaged in during those days, the answer is more likely to be “No”.

In circuit we can use the clock cycles to mimic days and can consider all three apps (CC, FPV, FCA) in the presence of flops to store the previous state driving by the clock. Now we are asking the reachability problem with latency of N cycles.

This analogy also illustrates the importance of initial states to determine a formal solution. If we ask the above question on a day when we have to go to the grocery store or visit the hospital versus a day spent at home watching Netflix, the answers will be different.

Another fun formulation of the problem is to view it as a hardware security “data integrity” problem. Suppose we consider the infected people to be untrusted elements and the non-infected people (or maybe just me) to be the trusted elements as we do in the Formal Security Verification (FSV) application. Clearly any propagation from non-trusted to trusted would present a data integrity problem or exposure to the virus, in this analogy.

I hope you found this analogy entertaining and will think of it next time you consider reachability analysis.

I wish everyone to stay safe and healthy.