In the following sections we will present case studies that illustrate the use of Pacti for different applications.
We present a case study to evaluate the perception system of an autonomous car using the quotient operator.
A case study on multi-agent path finding (MAPF) where multiple agents need to reach their target location on a grid world according to a conflict-free strategy. We treat each time step as our viewpoint to find a solution that satisfies the agents' dynamics and collision constraints using the merge operator.
A case study on modeling the specifications of a biological circuit and speed up the experimental design process by finding optimal components to use from a library of parts. In the case study, we first build a characterized library of parts as assume-guarantee contracts using existing experimental data from the literature.With the use of Pacti, we demonstrate how scientists may describe the desired top-level behavior as contracts and then computationally choose from a library of available parts to ensure that the components meet the top-level system specification. For the engineered bacteria case study, we find the specification of the sensors that meet the top-level criteria on fold-change of the circuit response. Finally, we also show how we can find the specifications of missing parts in a system. In synthetic biology, it is common to have parts in the system for which no characterization data is available. Using quotient operation on contracts, we can find the constraints that this missing part must satisfy to meet the desired top-level criteria.
A case study on word length analysis and optimization for digital signal processing circuit design.
We demonstrate the application of Pacti in modeling a context-sensitive grammar for generating three-dimensional topologies for Unmanned Aerial Vehicles (UAVs).
A case study on modeling the specifications of autonomous tasks for a planning/scheduling onboard of a space mission system.
A case study on modeling a simplified timeline of the Mars 2020 Entry-Descent-Landing.