Programmable logic controllers (PLCs) are widely used in industrial systems to control physical plants. Ensuring their correctness is important due to their safety-critical nature. However, existing formal analysis techniques focus on individual PLC programs in isolation, often neglecting interactions with physical plants and networked communication between different controllers. This limitation poses significant challenges in analyzing real-world industrial systems, where continuous dynamics and distributed coordination play a central role. This paper presents a unified formal framework that integrates discrete PLC semantics, networked communication, and continuous physical behaviors. To mitigate state explosion in model checking, we apply partial order reduction to reduce the number of explored states while preserving correctness. Our framework enables precise analysis of PLC-based cyber-physical systems.