Partial order reduction
কম্পিউটার বিজ্ঞানে, আংশিক ক্রম হ্রাস একটি মডেল চেকিং বা স্বয়ংক্রিয় পরিকল্পনা এবং সময়সূচী অ্যালগরিদম দ্বারা অনুসন্ধান করার জন্য রাজ্য-স্থানের আকার হ্রাস করার একটি কৌশল। এটি একযোগে সম্পাদিত রূপান্তরগুলির বিনিময়শীলতাকে কাজে লাগায় যার ফলস্বরূপ বিভিন্ন ক্রমে কার্যকর করা হলে একই অবস্থা হয়। এক্সপ্লিসিট স্টেট স্পেস এক্সপ্লোরেশন-এ, আংশিক ক্রম হ্রাস সাধারণত সমস্ত সক্ষম ট্রানজিশনের একটি প্রতিনিধি উপসেট সম্প্রসারণের নির্দিষ্ট কৌশলকে বোঝায়। এই কৌশলটিকে প্রতিনিধিদের সাথে মডেল চেকিং হিসাবেও বর্ণনা করা হয়েছে। পদ্ধতির বিভিন্ন সংস্করণ রয়েছে, তথাকথিত জেদী সেট পদ্ধতি, পর্যাপ্ত সেট পদ্ধতি এবং স্থায়ী সেট পদ্ধতি। প্রতিনিধিদের সাথে মডেল চেকিংয়ের একটি উদাহরণ হল প্রশস্ত সেট। তাদের গঠন নির্ভরতার একটি পৃথক ধারণার উপর নির্ভর করে। দুটি রূপান্তরকে স্বাধীন হিসাবে বিবেচনা করা হয় যদি তারা পারস্পরিকভাবে সক্ষম হলে অন্যটিকে নিষ্ক্রিয় করতে না পারে। যে ক্রমেই এগুলি কার্যকর করা হয় তা নির্বিশেষে উভয়ের কার্যকরকরণ একটি অনন্য অবস্থায় ফলাফল দেয়। যে রূপান্তরগুলি স্বাধীন নয়, সেগুলি নির্ভরশীল। বাস্তবে স্ট্যাটিক বিশ্লেষণ ব্যবহার করে নির্ভরশীলতার আনুমানিক হিসাব করা হয়। বিভিন্ন উদ্দেশ্যে পর্যাপ্ত সেটগুলি একটি নির্দিষ্ট অবস্থায় কখন ট্রানজিশনের একটি সেট "পর্যাপ্ত" হয় তার শর্ত দিয়ে সংজ্ঞায়িত করা যেতে পারে। সি0 সি1 যদি কোনও রূপান্তর কোনও রূপান্তর সম্পর্কের উপর নির্ভর করে, তবে পর্যাপ্ত সেটের কিছু রূপান্তর কার্যকর না হওয়া পর্যন্ত এই রূপান্তরটি আহ্বান করা যাবে না। রাজ্যের সমস্ত অচলাবস্থা বজায় রাখার জন্য সি0 এবং সি1 শর্তই যথেষ্ট। আরও সূক্ষ্ম বৈশিষ্ট্য সংরক্ষণের জন্য আরও বিধিনিষেধের প্রয়োজন। উদাহরণস্বরূপ, রৈখিক সাময়িক যুক্তির বৈশিষ্ট্যগুলি সংরক্ষণ করার জন্য, নিম্নলিখিত দুটি শর্ত প্রয়োজনঃ সি 2 যদি, পর্যাপ্ত সেটের প্রতিটি রূপান্তর অদৃশ্য হয়। সি3 একটি চক্র অনুমোদিত নয় যদি এতে এমন একটি অবস্থা থাকে যেখানে কিছু রূপান্তর সক্ষম করা হয়, তবে চক্রের কোনও অবস্থার জন্য পর্যাপ্ত (গুলি) অন্তর্ভুক্ত করা হয় না। এই শর্তগুলি একটি পর্যাপ্ত সেটের জন্য যথেষ্ট, তবে প্রয়োজনীয় শর্ত নয়। একগুঁয়ে সেট একগুঁয়ে সেট একটি স্পষ্ট স্বাধীনতা সম্পর্কের কোনও ব্যবহার করে না। পরিবর্তে এগুলি কেবল ক্রিয়াগুলির ক্রমের উপর বিনিময়শীলতার মাধ্যমে সংজ্ঞায়িত করা হয়। একটি সেট s-এ (দুর্বলভাবে) জেদী হয়, যদি নিম্নলিখিতটি ধরে থাকে। D0, যদি ক্রমটি কার্যকর করা সম্ভব হয় এবং অবস্থার দিকে নিয়ে যায়, তবে ক্রমটি কার্যকর করা সম্ভব এবং অবস্থার দিকে নিয়ে যাবে। D1 হয় একটি অচলাবস্থা, অথবা এমন যে, এর কার্যকরকরণ সম্ভব। এই শর্তগুলি সমস্ত ডেডলক সংরক্ষণের জন্য যথেষ্ট, ঠিক যেমন সি0 এবং সি1 পর্যাপ্ত নির্ধারিত পদ্ধতিতে রয়েছে। তবে এগুলি কিছুটা দুর্বল, এবং এর ফলে ছোট সেট হতে পারে। সি2 এবং সি3 শর্তগুলি পর্যাপ্ত সেট পদ্ধতিতে যা রয়েছে তার থেকে আরও দুর্বল হতে পারে, তবে জেদী সেট পদ্ধতিটি সি2 এবং সি3-এর সাথে সামঞ্জস্যপূর্ণ। অন্যান্য আংশিক ক্রম হ্রাসের জন্য অন্যান্য স্বরলিপিও রয়েছে। সাধারণভাবে ব্যবহৃত একটি হল স্থায়ী সেট/স্লিপ সেট অ্যালগরিদম। প্যাট্রিস গডফ্রয়েডের গবেষণাপত্রে বিস্তারিত তথ্য পাওয়া যাবে। প্রতীকী মডেল চেকিং-এ, আরও সীমাবদ্ধতা (গার্ড শক্তিশালীকরণ) যোগ করে আংশিক ক্রম হ্রাস অর্জন করা যেতে পারে। আংশিক অর্ডার হ্রাসের আরও প্রয়োগগুলি স্বয়ংক্রিয় পরিকল্পনার সাথে জড়িত। উদ্ধৃতি রেফারেন্স মডেল চেকিং