  The Supreme Court plays an extremely critical role in ensuring adherence to
the rule of law and in strengthening the democracy. Due to this reason,
modeling and analysis of small group interactions in the courtroom setting is
an important task as it can help in understanding court decision-making. We
apply probabilistic model checking for the modeling and analysis of temporal
interaction dynamics in the context of the Supreme Court of the United States.
We have used the transcripts of the oral arguments of cases from the Supreme
Court for constructing a discrete-time Markov reward model (DTMRM). Next, we
formulate interesting queries over interaction by using probabilistic
computation tree logic (PCTL) and PCTL with rewards and verify them using a
probabilistic symbolic model checker (PRISM). Our experimental results show
that probabilistic model checking is very effective in identifying trends,
hidden patterns, and how justices behave during the trials. These results not
only provide valuable feedback to the justices but may also be used by the
advocates and law students for finding better ways to present their arguments
in the court.
