• Article  

      Coverage analysis of mobile agent trajectory via state-based opacity formulations 

      Saboori, A.; Hadjicostis, Christoforos N. (2011)
      This paper performs coverage analysis of mobile agent trajectory utilizing discrete event system models and employing state-based notions of opacity. Non-deterministic finite automata with partial observation on their ...
    • Article  

      Current-state opacity formulations in probabilistic finite automata 

      Saboori, A.; Hadjicostis, Christoforos N. (2014)
      A system is said to be current-state opaque if the entrance of the system state to a set of secret states remains opaque (uncertain) to an intruder - at least until the system leaves the set of secret states. This notion ...
    • Conference Object  

      Initial state opacity in stochastic des 

      Keroglou, C.; Hadjicostis, Christoforos N. (2013)
      A non-deterministic finite automaton is initial-state opaque if the membership of its true initial state to a given set of secret states S remains opaque (i.e., uncertain) to an intruder who observes system activity through ...
    • Conference Object  

      Notions of security and opacity in discrete event systems 

      Saboori, A.; Hadjicostis, Christoforos N. (2007)
      In this paper, we follow a state-based approach to extend the notion of opacity in computer security to discrete event systems. A system is (S, P)-opaque if the evolution of its true state through a set of secret states S ...
    • Article  

      On the history of diagnosability and opacity in discrete event systems 

      Lafortune, S.; Lin, F.; Hadjicostis, Christoforos N. (2018)
      This paper presents historical remarks on key projects and papers that led to the development of a theory of event diagnosis for discrete event systems modeled by finite-state automata or Petri nets in the 1990s. The goal ...
    • Conference Object  

      Opacity formulations and verification in discrete event systems 

      Hadjicostis, Christoforos N.; Keroglou, C. (Institute of Electrical and Electronics Engineers Inc., 2014)
      In many emerging security applications, a property of a system, that may reveal important details about its behaviour, needs to be kept secret (opaque) to outside observers (intruders). Motivated by such applications, ...
    • Conference Object  

      Opacity verification in stochastic discrete event systems 

      Saboori, A.; Hadjicostis, Christoforos N. (2010)
      Motivated by security and privacy considerations in applications of discrete event systems, various notions of opacity have been introduced. Specifically, a system is said to be current-state opaque if the entrance of the ...
    • Conference Object  

      Opacity-enforcing supervisory strategies for secure discrete event systems 

      Saboori, A.; Hadjicostis, Christoforos N. (2008)
      Initial-state opacity emerges as a key property in numerous security applications of discrete event systems including key-stream generators for cryptographic protocols. Specifically, a system is initial-state opaque if the ...
    • Article  

      Opacity-enforcing supervisory strategies via state estimator constructions 

      Saboori, A.; Hadjicostis, Christoforos N. (2012)
      State-based notions of opacity, such as initial-state opacity and infinite-step opacity, emerge as key properties in numerous security applications of discrete event systems. We consider systems that are modeled as partially ...
    • Conference Object  

      Probabilistic system opacity in discrete event systems 

      Keroglou, C.; Hadjicostis, Christoforos N. (Institute of Electrical and Electronics Engineers Inc., 2016)
      In many emerging security applications, a system designer frequently needs to ensure that a certain property of a given system (that may reveal important details about the system's operation) be kept secret (opaque) to ...
    • Article  

      Probabilistic system opacity in discrete event systems 

      Keroglou, C.; Hadjicostis, Christoforos N. (2018)
      In many emerging security applications, a system designer frequently needs to ensure that a certain property of a given system (that may reveal important details about the system’s operation) be kept secret (opaque) to ...
    • Conference Object  

      Reduced-complexity verification for initial-state opacity in modular discrete event systems 

      Saboori, A.; Hadjicostis, Christoforos N. (2010)
      In this paper, we propose and analyze reduced-complexity methodologies for verifying initial-state opacity in modular discrete event systems. Initial-state opacity requires that the membership of the system initial state ...
    • Conference Object  

      Verification of infinite-step opacity and analysis of its complexity 

      Saboori, A.; Hadjicostis, Christoforos N. (2009)
      In this paper, we formulate, analyze, and devise methodologies to verify the notion of infinite-step opacity in discrete event systems that are modeled as (possibly non-deterministic) finite automata with partial observation ...
    • Article  

      Verification of infinite-step opacity and complexity considerations 

      Saboori, A.; Hadjicostis, Christoforos N. (2012)
      We describe and analyze the complexity of verifying the notion of infinite-step opacity in systems that are modeled as non-deterministic finite automata with partial observation on their transitions. Specifically, a system ...
    • Conference Object  

      Verification of initial-state opacity in security applications of DES 

      Saboori, A.; Hadjicostis, Christoforos N. (2008)
      Motivated by security applications where the initial state of a system needs to be kept secret (opaque) to outside observers (intruders), we formulate, analyze and verify the notion of initial-state opacity in discrete ...
    • Article  

      Verification of initial-state opacity in security applications of discrete event systems 

      Saboori, A.; Hadjicostis, Christoforos N. (2013)
      In this paper, we formulate and analyze methodologies for verifying the notion of initial-state opacity in discrete event systems that are modeled as non-deterministic finite automata with partial observation on their ...
    • Article  

      Verification of K-step opacity and analysis of its complexity 

      Saboori, A.; Hadjicostis, Christoforos N. (2011)
      Motivated by security and privacy considerations in a variety of applications of discrete event systems, we describe and analyze the computational complexity required for verifying the notion of K-step opacity for systems ...
    • Conference Object  

      Verification of K-step opacity and analysis of its complexity 

      Saboori, A.; Hadjicostis, Christoforos N. (2009)
      In this paper, we analyze the verification of K-step opacity in discrete event systems that are modeled as (possibly non-deterministic) finite automata with partial observation on their transitions. A system is K-step ...