Counterexample Generation for Safety, Ethics, Security & Synthesis
Safety-critical cyber-physical systems — autonomous vehicles, medical devices, aerospace controllers — must be certified before deployment. Our research addresses this challenge through falsification: using black-box optimization to systematically search for inputs that cause a system to violate its specifications, expressed as temporal logic formulas (STL, MTL, HyperSTL).
We developed the Part-X family of stochastic algorithms, which provide probabilistic guarantees on the absence of counterexamples within a specified confidence level. Extensions include conBO for systems with conjunctive (multi-property) requirements and HyperPart-X for parameter mining in parametric temporal logic — enabling formal certification from automatically generated test evidence. More recently, we have expanded this line of work to address synthesis and ethical requirements, making verification applicable to a broader class of intelligent systems.
Representative Publications
- Chotalyia, S., Khandait, T., & Pedrielli, G. Conjunctive Bayesian Optimization (conBO): An application to Cyber-Physical Systems Verification with Conjunctive Requirements. ACM Trans. Cyber-Physical Systems, 2026.
- Abou-Mrad, C., Khandait, T., Pedrielli, G., & Abbas, H. Falsification and Control of CPS using the Language Set of Discrete-Time Temporal Logic. ICCPS 2025.
- Khandait, T. & Pedrielli, G. HyperPart-X: Probabilistic Guarantees for Parameter Mining of Signal Temporal Logic Formulas in CPS. RV 2024.
- Pedrielli, G., Khandait, T., Cao, Y., et al. Part-X: A family of stochastic algorithms for search-based test generation with probabilistic guarantees. IEEE TASE, 2023. DOI
- Thibeault, Q., Khandait, T., Pedrielli, G., & Fainekos, G. Search based testing for code coverage and falsification in cyber-physical systems. IEEE CASE 2023. DOI
Automatic Model Recovery
A digital twin is only as good as the simulation model behind it. Building and maintaining high-fidelity models for complex systems is a bottleneck — it requires deep domain expertise and substantial manual effort that does not scale. Our research tackles this challenge through automatic model recovery: data-driven approaches that reconstruct or generate simulation models directly from observed system behavior.
Our Map-GPT project, in collaboration with Intel, develops AI-driven pipelines to automatically generate and accelerate digital twins for semiconductor test systems. In parallel, our generative simulation framework establishes the theoretical foundations for generative digital twins — models that can produce realistic synthetic scenarios for supply chain and manufacturing applications, enabling planning and decision-making without requiring full physical model specification.
Representative Publications
- Chotaliya, S., Fowler, J., Pedrielli, G., et al. A Foundational Framework for Generative Simulation Models: Pathway to Generative Digital Twins for Supply Chain. WSC 2025.
Manufacturing & Semiconductors
Modern manufacturing — especially semiconductor fabrication — operates under extreme complexity: tight tolerances, high equipment costs, and intricate scheduling constraints. We develop digital twin methodologies that model, optimize, and control these processes. Our DTFab framework addresses optimal reticle management in semiconductor photolithography, a critical cost driver in chip production, by embedding digital twin simulation within an optimization loop.
At the systems level, we develop cyber-coordinated analytical frameworks for multi-stage distributed future manufacturing (NSF FMRG) and participate in the NSF Industry–University Cooperative Research Center on Digital Twins for Manufacturing (IUCRC). These efforts target the design of resilient, data-driven manufacturing systems that can adapt to disruptions and uncertainty in real time.
Representative Publications
- Sivasubramanian, C.K., Dodge, R., Ramani, A., et al. DTFab: A digital twin based approach for optimal reticle management in semiconductor photolithography. Journal of Systems Science and Systems Engineering, 2023. DOI
- Chotaliya, S., Fowler, J., Pedrielli, G., et al. A Foundational Framework for Generative Simulation Models: Pathway to Generative Digital Twins for Supply Chain. WSC 2025.